Theorem cfpwsdom 9663

Description: A corollary of Konig's Theorem konigth 9648. 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 6878	. . . . . . . . 9 ⊢ (𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ V
2	1	cardid 9626	. . . . . . . 8 ⊢ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚 (ℵ‘𝐴))
3	2	ensymi 8214	. . . . . . 7 ⊢ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≈ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))
4		fvex 6392	. . . . . . . . . . . . . 14 ⊢ (ℵ‘𝐴) ∈ V
5	4	canth2 8324	. . . . . . . . . . . . 13 ⊢ (ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴)
6	4	pw2en 8278	. . . . . . . . . . . . 13 ⊢ 𝒫 (ℵ‘𝐴) ≈ (2𝑜 ↑𝑚 (ℵ‘𝐴))
7		sdomentr 8305	. . . . . . . . . . . . 13 ⊢ (((ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2𝑜 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)))
8	5, 6, 7	mp2an 683	. . . . . . . . . . . 12 ⊢ (ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴))
9		mapdom1 8336	. . . . . . . . . . . 12 ⊢ (2𝑜 ≼ 𝐵 → (2𝑜 ↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
10		sdomdomtr 8304	. . . . . . . . . . . 12 ⊢ (((ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)) ∧ (2𝑜 ↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
11	8, 9, 10	sylancr 581	. . . . . . . . . . 11 ⊢ (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
12		ficard 9644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ V → ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω))
13	1, 12	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω)
14		isfinite 8768	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ω)
15		sdomdom 8192	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ω → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
16	14, 15	sylbi 208	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
17	13, 16	sylbir 226	. . . . . . . . . . . . . . 15 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
18		alephgeom 9160	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On ↔ ω ⊆ (ℵ‘𝐴))
19		alephon 9147	. . . . . . . . . . . . . . . . 17 ⊢ (ℵ‘𝐴) ∈ On
20		ssdomg 8210	. . . . . . . . . . . . . . . . 17 ⊢ ((ℵ‘𝐴) ∈ On → (ω ⊆ (ℵ‘𝐴) → ω ≼ (ℵ‘𝐴)))
21	19, 20	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (ω ⊆ (ℵ‘𝐴) → ω ≼ (ℵ‘𝐴))
22	18, 21	sylbi 208	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → ω ≼ (ℵ‘𝐴))
23		domtr 8217	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω ∧ ω ≼ (ℵ‘𝐴)) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴))
24	17, 22, 23	syl2an 589	. . . . . . . . . . . . . 14 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴))
25		domnsym 8297	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴) → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
26	24, 25	syl 17	. . . . . . . . . . . . 13 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
27	26	expcom 402	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴))))
28	27	con2d 131	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → ((ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)) → ¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω))
29		cardidm 9040	. . . . . . . . . . . 12 ⊢ (card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))
30		iscard3 9171	. . . . . . . . . . . . 13 ⊢ ((card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ))
31		elun 3917	. . . . . . . . . . . . 13 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ) ↔ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
32		df-or 874	. . . . . . . . . . . . 13 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ) ↔ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
33	30, 31, 32	3bitri 288	. . . . . . . . . . . 12 ⊢ ((card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↔ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
34	29, 33	mpbi 221	. . . . . . . . . . 11 ⊢ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ)
35	11, 28, 34	syl56 36	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
36		alephfnon 9143	. . . . . . . . . . 11 ⊢ ℵ Fn On
37		fvelrnb 6436	. . . . . . . . . . 11 ⊢ (ℵ Fn On → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
38	36, 37	ax-mp 5	. . . . . . . . . 10 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
39	35, 38	syl6ib 242	. . . . . . . . 9 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
40		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) = (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦)))
41	40	pwcfsdom 9662	. . . . . . . . . . 11 ⊢ (ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥)))
42		id 22	. . . . . . . . . . . 12 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
43		fveq2 6379	. . . . . . . . . . . . 13 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (cf‘(ℵ‘𝑥)) = (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
44	42, 43	oveq12d 6864	. . . . . . . . . . . 12 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥))) = ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
45	42, 44	breq12d 4824	. . . . . . . . . . 11 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥))) ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
46	41, 45	mpbii 224	. . . . . . . . . 10 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
47	46	rexlimivw 3176	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
48	39, 47	syl6 35	. . . . . . . 8 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
49	48	imp 395	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
50		ensdomtr 8307	. . . . . . 7 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≈ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∧ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
51	3, 49, 50	sylancr 581	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
52		fvex 6392	. . . . . . . . 9 ⊢ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V
53	52	enref 8197	. . . . . . . 8 ⊢ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
54		mapen 8335	. . . . . . . 8 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚 (ℵ‘𝐴)) ∧ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
55	2, 53, 54	mp2an 683	. . . . . . 7 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
56		cfpwsdom.1	. . . . . . . 8 ⊢ 𝐵 ∈ V
57		mapxpen 8337	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ (ℵ‘𝐴) ∈ On ∧ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V) → ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
58	56, 19, 52, 57	mp3an 1585	. . . . . . 7 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
59	55, 58	entri 8218	. . . . . 6 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
60		sdomentr 8305	. . . . . 6 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ∧ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
61	51, 59, 60	sylancl 580	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
62	4	xpdom2 8266	. . . . . . . . . 10 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)))
63	18	biimpi 207	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → ω ⊆ (ℵ‘𝐴))
64		infxpen 9092	. . . . . . . . . . 11 ⊢ (((ℵ‘𝐴) ∈ On ∧ ω ⊆ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴))
65	19, 63, 64	sylancr 581	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴))
66		domentr 8223	. . . . . . . . . 10 ⊢ ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)) ∧ ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴))
67	62, 65, 66	syl2an 589	. . . . . . . . 9 ⊢ (((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴))
68		nsuceq0 5990	. . . . . . . . . . 11 ⊢ suc 1𝑜 ≠ ∅
69		dom0 8299	. . . . . . . . . . 11 ⊢ (suc 1𝑜 ≼ ∅ ↔ suc 1𝑜 = ∅)
70	68, 69	nemtbir 3032	. . . . . . . . . 10 ⊢ ¬ suc 1𝑜 ≼ ∅
71		df-2o 7769	. . . . . . . . . . . . . 14 ⊢ 2𝑜 = suc 1𝑜
72	71	breq1i 4818	. . . . . . . . . . . . 13 ⊢ (2𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ 𝐵)
73		breq2 4815	. . . . . . . . . . . . 13 ⊢ (𝐵 = ∅ → (suc 1𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ ∅))
74	72, 73	syl5bb 274	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → (2𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ ∅))
75	74	biimpcd 240	. . . . . . . . . . 11 ⊢ (2𝑜 ≼ 𝐵 → (𝐵 = ∅ → suc 1𝑜 ≼ ∅))
76	75	adantld 484	. . . . . . . . . 10 ⊢ (2𝑜 ≼ 𝐵 → ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅) → suc 1𝑜 ≼ ∅))
77	70, 76	mtoi 190	. . . . . . . . 9 ⊢ (2𝑜 ≼ 𝐵 → ¬ (((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅))
78		mapdom2 8342	. . . . . . . . 9 ⊢ ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴) ∧ ¬ (((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅)) → (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
79	67, 77, 78	syl2an 589	. . . . . . . 8 ⊢ ((((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
80		domnsym 8297	. . . . . . . 8 ⊢ ((𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
81	79, 80	syl 17	. . . . . . 7 ⊢ ((((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) ∧ 2𝑜 ≼ 𝐵) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
82	81	expl 449	. . . . . 6 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))))
83	82	com12 32	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))))
84	61, 83	mt2d 133	. . . 4 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ¬ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴))
85		domtri 9635	. . . . . 6 ⊢ (((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V ∧ (ℵ‘𝐴) ∈ V) → ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
86	52, 4, 85	mp2an 683	. . . . 5 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
87	86	biimpri 219	. . . 4 ⊢ (¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴))
88	84, 87	nsyl2 144	. . 3 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
89	88	ex 401	. 2 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
90		fndm 6170	. . . . . 6 ⊢ (ℵ Fn On → dom ℵ = On)
91	36, 90	ax-mp 5	. . . . 5 ⊢ dom ℵ = On
92	91	eleq2i 2836	. . . 4 ⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On)
93		ndmfv 6409	. . . 4 ⊢ (¬ 𝐴 ∈ dom ℵ → (ℵ‘𝐴) = ∅)
94	92, 93	sylnbir 322	. . 3 ⊢ (¬ 𝐴 ∈ On → (ℵ‘𝐴) = ∅)
95		1n0 7784	. . . . . 6 ⊢ 1𝑜 ≠ ∅
96		1onn 7928	. . . . . . . 8 ⊢ 1𝑜 ∈ ω
97	96	elexi 3366	. . . . . . 7 ⊢ 1𝑜 ∈ V
98	97	0sdom 8302	. . . . . 6 ⊢ (∅ ≺ 1𝑜 ↔ 1𝑜 ≠ ∅)
99	95, 98	mpbir 222	. . . . 5 ⊢ ∅ ≺ 1𝑜
100		id 22	. . . . . 6 ⊢ ((ℵ‘𝐴) = ∅ → (ℵ‘𝐴) = ∅)
101		oveq2 6854	. . . . . . . . . . 11 ⊢ ((ℵ‘𝐴) = ∅ → (𝐵 ↑𝑚 (ℵ‘𝐴)) = (𝐵 ↑𝑚 ∅))
102		map0e 8102	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → (𝐵 ↑𝑚 ∅) = 1𝑜)
103	56, 102	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐵 ↑𝑚 ∅) = 1𝑜
104	101, 103	syl6eq 2815	. . . . . . . . . 10 ⊢ ((ℵ‘𝐴) = ∅ → (𝐵 ↑𝑚 (ℵ‘𝐴)) = 1𝑜)
105	104	fveq2d 6383	. . . . . . . . 9 ⊢ ((ℵ‘𝐴) = ∅ → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) = (card‘1𝑜))
106		cardnn 9044	. . . . . . . . . 10 ⊢ (1𝑜 ∈ ω → (card‘1𝑜) = 1𝑜)
107	96, 106	ax-mp 5	. . . . . . . . 9 ⊢ (card‘1𝑜) = 1𝑜
108	105, 107	syl6eq 2815	. . . . . . . 8 ⊢ ((ℵ‘𝐴) = ∅ → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) = 1𝑜)
109	108	fveq2d 6383	. . . . . . 7 ⊢ ((ℵ‘𝐴) = ∅ → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (cf‘1𝑜))
110		df-1o 7768	. . . . . . . . 9 ⊢ 1𝑜 = suc ∅
111	110	fveq2i 6382	. . . . . . . 8 ⊢ (cf‘1𝑜) = (cf‘suc ∅)
112		0elon 5963	. . . . . . . . 9 ⊢ ∅ ∈ On
113		cfsuc 9336	. . . . . . . . 9 ⊢ (∅ ∈ On → (cf‘suc ∅) = 1𝑜)
114	112, 113	ax-mp 5	. . . . . . . 8 ⊢ (cf‘suc ∅) = 1𝑜
115	111, 114	eqtri 2787	. . . . . . 7 ⊢ (cf‘1𝑜) = 1𝑜
116	109, 115	syl6eq 2815	. . . . . 6 ⊢ ((ℵ‘𝐴) = ∅ → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = 1𝑜)
117	100, 116	breq12d 4824	. . . . 5 ⊢ ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ↔ ∅ ≺ 1𝑜))
118	99, 117	mpbiri 249	. . . 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 197   ∧ wa 384   ∨ wo 873   = wceq 1652   ∈ wcel 2155   ≠ wne 2937  ∃wrex 3056  Vcvv 3350   ∪ cun 3732   ⊆ wss 3734  ∅c0 4081  𝒫 cpw 4317   class class class wbr 4811   ↦ cmpt 4890   × cxp 5277  dom cdm 5279  ran crn 5280  Oncon0 5910  suc csuc 5912   Fn wfn 6065  ‘cfv 6070  (class class class)co 6846  ωcom 7267  1_𝑜c1o 7761  2_𝑜c2o 7762   ↑_𝑚 cmap 8064   ≈ cen 8161   ≼ cdom 8162   ≺ csdm 8163  Fincfn 8164  harchar 8672  cardccrd 9016  ℵcale 9017  cfccf 9018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757  ax-ac2 9542

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-smo 7651  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-ixp 8118  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-oi 8626  df-har 8674  df-card 9020  df-aleph 9021  df-cf 9022  df-acn 9023  df-ac 9194

This theorem is referenced by:  alephom  9664