Theorem cfpwsdom 9406

Description: A corollary of Konig's Theorem konigth 9391. Theorem 11.29 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.)

Hypothesis

Ref	Expression
cfpwsdom.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
cfpwsdom	⊢ (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))

Proof of Theorem cfpwsdom

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 6678	. . . . . . . . 9 ⊢ (𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ V
2	1	cardid 9369	. . . . . . . 8 ⊢ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚 (ℵ‘𝐴))
3	2	ensymi 8006	. . . . . . 7 ⊢ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≈ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))
4		fvex 6201	. . . . . . . . . . . . . 14 ⊢ (ℵ‘𝐴) ∈ V
5	4	canth2 8113	. . . . . . . . . . . . 13 ⊢ (ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴)
6	4	pw2en 8067	. . . . . . . . . . . . 13 ⊢ 𝒫 (ℵ‘𝐴) ≈ (2𝑜 ↑𝑚 (ℵ‘𝐴))
7		sdomentr 8094	. . . . . . . . . . . . 13 ⊢ (((ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2𝑜 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)))
8	5, 6, 7	mp2an 708	. . . . . . . . . . . 12 ⊢ (ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴))
9		mapdom1 8125	. . . . . . . . . . . 12 ⊢ (2𝑜 ≼ 𝐵 → (2𝑜 ↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
10		sdomdomtr 8093	. . . . . . . . . . . 12 ⊢ (((ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)) ∧ (2𝑜 ↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
11	8, 9, 10	sylancr 695	. . . . . . . . . . 11 ⊢ (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
12		ficard 9387	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ V → ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω))
13	1, 12	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω)
14		isfinite 8549	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ω)
15		sdomdom 7983	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ω → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
16	14, 15	sylbi 207	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
17	13, 16	sylbir 225	. . . . . . . . . . . . . . 15 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
18		alephgeom 8905	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On ↔ ω ⊆ (ℵ‘𝐴))
19		alephon 8892	. . . . . . . . . . . . . . . . 17 ⊢ (ℵ‘𝐴) ∈ On
20		ssdomg 8001	. . . . . . . . . . . . . . . . 17 ⊢ ((ℵ‘𝐴) ∈ On → (ω ⊆ (ℵ‘𝐴) → ω ≼ (ℵ‘𝐴)))
21	19, 20	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (ω ⊆ (ℵ‘𝐴) → ω ≼ (ℵ‘𝐴))
22	18, 21	sylbi 207	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → ω ≼ (ℵ‘𝐴))
23		domtr 8009	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω ∧ ω ≼ (ℵ‘𝐴)) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴))
24	17, 22, 23	syl2an 494	. . . . . . . . . . . . . 14 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴))
25		domnsym 8086	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴) → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
26	24, 25	syl 17	. . . . . . . . . . . . 13 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
27	26	expcom 451	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴))))
28	27	con2d 129	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → ((ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)) → ¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω))
29		cardidm 8785	. . . . . . . . . . . 12 ⊢ (card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))
30		iscard3 8916	. . . . . . . . . . . . 13 ⊢ ((card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ))
31		elun 3753	. . . . . . . . . . . . 13 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ) ↔ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
32		df-or 385	. . . . . . . . . . . . 13 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ) ↔ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
33	30, 31, 32	3bitri 286	. . . . . . . . . . . 12 ⊢ ((card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↔ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
34	29, 33	mpbi 220	. . . . . . . . . . 11 ⊢ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ)
35	11, 28, 34	syl56 36	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
36		alephfnon 8888	. . . . . . . . . . 11 ⊢ ℵ Fn On
37		fvelrnb 6243	. . . . . . . . . . 11 ⊢ (ℵ Fn On → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
38	36, 37	ax-mp 5	. . . . . . . . . 10 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
39	35, 38	syl6ib 241	. . . . . . . . 9 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
40		eqid 2622	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) = (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦)))
41	40	pwcfsdom 9405	. . . . . . . . . . 11 ⊢ (ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥)))
42		id 22	. . . . . . . . . . . 12 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
43		fveq2 6191	. . . . . . . . . . . . 13 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (cf‘(ℵ‘𝑥)) = (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
44	42, 43	oveq12d 6668	. . . . . . . . . . . 12 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥))) = ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
45	42, 44	breq12d 4666	. . . . . . . . . . 11 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥))) ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
46	41, 45	mpbii 223	. . . . . . . . . 10 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
47	46	rexlimivw 3029	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
48	39, 47	syl6 35	. . . . . . . 8 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
49	48	imp 445	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
50		ensdomtr 8096	. . . . . . 7 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≈ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∧ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
51	3, 49, 50	sylancr 695	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
52		fvex 6201	. . . . . . . . 9 ⊢ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V
53	52	enref 7988	. . . . . . . 8 ⊢ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
54		mapen 8124	. . . . . . . 8 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚 (ℵ‘𝐴)) ∧ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
55	2, 53, 54	mp2an 708	. . . . . . 7 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
56		cfpwsdom.1	. . . . . . . 8 ⊢ 𝐵 ∈ V
57		mapxpen 8126	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ (ℵ‘𝐴) ∈ On ∧ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V) → ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
58	56, 19, 52, 57	mp3an 1424	. . . . . . 7 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
59	55, 58	entri 8010	. . . . . 6 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
60		sdomentr 8094	. . . . . 6 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ∧ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
61	51, 59, 60	sylancl 694	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
62	4	xpdom2 8055	. . . . . . . . . 10 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)))
63	18	biimpi 206	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → ω ⊆ (ℵ‘𝐴))
64		infxpen 8837	. . . . . . . . . . 11 ⊢ (((ℵ‘𝐴) ∈ On ∧ ω ⊆ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴))
65	19, 63, 64	sylancr 695	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴))
66		domentr 8015	. . . . . . . . . 10 ⊢ ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)) ∧ ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴))
67	62, 65, 66	syl2an 494	. . . . . . . . 9 ⊢ (((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴))
68		nsuceq0 5805	. . . . . . . . . . 11 ⊢ suc 1𝑜 ≠ ∅
69		dom0 8088	. . . . . . . . . . 11 ⊢ (suc 1𝑜 ≼ ∅ ↔ suc 1𝑜 = ∅)
70	68, 69	nemtbir 2889	. . . . . . . . . 10 ⊢ ¬ suc 1𝑜 ≼ ∅
71		df-2o 7561	. . . . . . . . . . . . . 14 ⊢ 2𝑜 = suc 1𝑜
72	71	breq1i 4660	. . . . . . . . . . . . 13 ⊢ (2𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ 𝐵)
73		breq2 4657	. . . . . . . . . . . . 13 ⊢ (𝐵 = ∅ → (suc 1𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ ∅))
74	72, 73	syl5bb 272	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → (2𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ ∅))
75	74	biimpcd 239	. . . . . . . . . . 11 ⊢ (2𝑜 ≼ 𝐵 → (𝐵 = ∅ → suc 1𝑜 ≼ ∅))
76	75	adantld 483	. . . . . . . . . 10 ⊢ (2𝑜 ≼ 𝐵 → ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅) → suc 1𝑜 ≼ ∅))
77	70, 76	mtoi 190	. . . . . . . . 9 ⊢ (2𝑜 ≼ 𝐵 → ¬ (((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅))
78		mapdom2 8131	. . . . . . . . 9 ⊢ ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴) ∧ ¬ (((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅)) → (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
79	67, 77, 78	syl2an 494	. . . . . . . 8 ⊢ ((((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
80		domnsym 8086	. . . . . . . 8 ⊢ ((𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
81	79, 80	syl 17	. . . . . . 7 ⊢ ((((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) ∧ 2𝑜 ≼ 𝐵) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
82	81	expl 648	. . . . . 6 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))))
83	82	com12 32	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))))
84	61, 83	mt2d 131	. . . 4 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ¬ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴))
85		domtri 9378	. . . . . 6 ⊢ (((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V ∧ (ℵ‘𝐴) ∈ V) → ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
86	52, 4, 85	mp2an 708	. . . . 5 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
87	86	biimpri 218	. . . 4 ⊢ (¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴))
88	84, 87	nsyl2 142	. . 3 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
89	88	ex 450	. 2 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
90		fndm 5990	. . . . . 6 ⊢ (ℵ Fn On → dom ℵ = On)
91	36, 90	ax-mp 5	. . . . 5 ⊢ dom ℵ = On
92	91	eleq2i 2693	. . . 4 ⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On)
93		ndmfv 6218	. . . 4 ⊢ (¬ 𝐴 ∈ dom ℵ → (ℵ‘𝐴) = ∅)
94	92, 93	sylnbir 321	. . 3 ⊢ (¬ 𝐴 ∈ On → (ℵ‘𝐴) = ∅)
95		1n0 7575	. . . . . 6 ⊢ 1𝑜 ≠ ∅
96		1onn 7719	. . . . . . . 8 ⊢ 1𝑜 ∈ ω
97	96	elexi 3213	. . . . . . 7 ⊢ 1𝑜 ∈ V
98	97	0sdom 8091	. . . . . 6 ⊢ (∅ ≺ 1𝑜 ↔ 1𝑜 ≠ ∅)
99	95, 98	mpbir 221	. . . . 5 ⊢ ∅ ≺ 1𝑜
100		id 22	. . . . . 6 ⊢ ((ℵ‘𝐴) = ∅ → (ℵ‘𝐴) = ∅)
101		oveq2 6658	. . . . . . . . . . 11 ⊢ ((ℵ‘𝐴) = ∅ → (𝐵 ↑𝑚 (ℵ‘𝐴)) = (𝐵 ↑𝑚 ∅))
102		map0e 7895	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → (𝐵 ↑𝑚 ∅) = 1𝑜)
103	56, 102	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐵 ↑𝑚 ∅) = 1𝑜
104	101, 103	syl6eq 2672	. . . . . . . . . 10 ⊢ ((ℵ‘𝐴) = ∅ → (𝐵 ↑𝑚 (ℵ‘𝐴)) = 1𝑜)
105	104	fveq2d 6195	. . . . . . . . 9 ⊢ ((ℵ‘𝐴) = ∅ → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) = (card‘1𝑜))
106		cardnn 8789	. . . . . . . . . 10 ⊢ (1𝑜 ∈ ω → (card‘1𝑜) = 1𝑜)
107	96, 106	ax-mp 5	. . . . . . . . 9 ⊢ (card‘1𝑜) = 1𝑜
108	105, 107	syl6eq 2672	. . . . . . . 8 ⊢ ((ℵ‘𝐴) = ∅ → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) = 1𝑜)
109	108	fveq2d 6195	. . . . . . 7 ⊢ ((ℵ‘𝐴) = ∅ → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (cf‘1𝑜))
110		df-1o 7560	. . . . . . . . 9 ⊢ 1𝑜 = suc ∅
111	110	fveq2i 6194	. . . . . . . 8 ⊢ (cf‘1𝑜) = (cf‘suc ∅)
112		0elon 5778	. . . . . . . . 9 ⊢ ∅ ∈ On
113		cfsuc 9079	. . . . . . . . 9 ⊢ (∅ ∈ On → (cf‘suc ∅) = 1𝑜)
114	112, 113	ax-mp 5	. . . . . . . 8 ⊢ (cf‘suc ∅) = 1𝑜
115	111, 114	eqtri 2644	. . . . . . 7 ⊢ (cf‘1𝑜) = 1𝑜
116	109, 115	syl6eq 2672	. . . . . 6 ⊢ ((ℵ‘𝐴) = ∅ → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = 1𝑜)
117	100, 116	breq12d 4666	. . . . 5 ⊢ ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ↔ ∅ ≺ 1𝑜))
118	99, 117	mpbiri 248	. . . 4 ⊢ ((ℵ‘𝐴) = ∅ → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
119	118	a1d 25	. . 3 ⊢ ((ℵ‘𝐴) = ∅ → (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
120	94, 119	syl 17	. 2 ⊢ (¬ 𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
121	89, 120	pm2.61i 176	1 ⊢ (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∃wrex 2913  Vcvv 3200   ∪ cun 3572   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158   class class class wbr 4653   ↦ cmpt 4729   × cxp 5112  dom cdm 5114  ran crn 5115  Oncon0 5723  suc csuc 5725   Fn wfn 5883  ‘cfv 5888  (class class class)co 6650  ωcom 7065  1_𝑜c1o 7553  2_𝑜c2o 7554   ↑_𝑚 cmap 7857   ≈ cen 7952   ≼ cdom 7953   ≺ csdm 7954  Fincfn 7955  harchar 8461  cardccrd 8761  ℵcale 8762  cfccf 8763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-ac2 9285

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-smo 7443  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-oi 8415  df-har 8463  df-card 8765  df-aleph 8766  df-cf 8767  df-acn 8768  df-ac 8939

This theorem is referenced by:  alephom  9407