Theorem cfpwsdom 9285

Description: A corollary of Konig's Theorem konigth 9270. 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 6577	. . . . . . . . 9 ⊢ (𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ V
2	1	cardid 9248	. . . . . . . 8 ⊢ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚 (ℵ‘𝐴))
3	2	ensymi 7892	. . . . . . 7 ⊢ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≈ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))
4		fvex 6113	. . . . . . . . . . . . . 14 ⊢ (ℵ‘𝐴) ∈ V
5	4	canth2 7998	. . . . . . . . . . . . 13 ⊢ (ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴)
6	4	pw2en 7952	. . . . . . . . . . . . 13 ⊢ 𝒫 (ℵ‘𝐴) ≈ (2𝑜 ↑𝑚 (ℵ‘𝐴))
7		sdomentr 7979	. . . . . . . . . . . . 13 ⊢ (((ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2𝑜 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)))
8	5, 6, 7	mp2an 704	. . . . . . . . . . . 12 ⊢ (ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴))
9		mapdom1 8010	. . . . . . . . . . . 12 ⊢ (2𝑜 ≼ 𝐵 → (2𝑜 ↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
10		sdomdomtr 7978	. . . . . . . . . . . 12 ⊢ (((ℵ‘𝐴) ≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)) ∧ (2𝑜 ↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
11	8, 9, 10	sylancr 694	. . . . . . . . . . 11 ⊢ (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
12		ficard 9266	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ V → ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω))
13	1, 12	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω)
14		isfinite 8432	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ω)
15		sdomdom 7869	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ω → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
16	14, 15	sylbi 206	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ∈ Fin → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
17	13, 16	sylbir 224	. . . . . . . . . . . . . . 15 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω)
18		alephgeom 8788	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On ↔ ω ⊆ (ℵ‘𝐴))
19		alephon 8775	. . . . . . . . . . . . . . . . 17 ⊢ (ℵ‘𝐴) ∈ On
20		ssdomg 7887	. . . . . . . . . . . . . . . . 17 ⊢ ((ℵ‘𝐴) ∈ On → (ω ⊆ (ℵ‘𝐴) → ω ≼ (ℵ‘𝐴)))
21	19, 20	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (ω ⊆ (ℵ‘𝐴) → ω ≼ (ℵ‘𝐴))
22	18, 21	sylbi 206	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → ω ≼ (ℵ‘𝐴))
23		domtr 7895	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ ω ∧ ω ≼ (ℵ‘𝐴)) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴))
24	17, 22, 23	syl2an 493	. . . . . . . . . . . . . 14 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴))
25		domnsym 7971	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ≼ (ℵ‘𝐴) → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
26	24, 25	syl 17	. . . . . . . . . . . . 13 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)))
27	26	expcom 450	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ On → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → ¬ (ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴))))
28	27	con2d 128	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → ((ℵ‘𝐴) ≺ (𝐵 ↑𝑚 (ℵ‘𝐴)) → ¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω))
29		cardidm 8668	. . . . . . . . . . . 12 ⊢ (card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))
30		iscard3 8799	. . . . . . . . . . . . 13 ⊢ ((card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ))
31		elun 3715	. . . . . . . . . . . . 13 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ) ↔ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
32		df-or 384	. . . . . . . . . . . . 13 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ) ↔ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
33	30, 31, 32	3bitri 285	. . . . . . . . . . . 12 ⊢ ((card‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↔ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
34	29, 33	mpbi 219	. . . . . . . . . . 11 ⊢ (¬ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ)
35	11, 28, 34	syl56 35	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ))
36		alephfnon 8771	. . . . . . . . . . 11 ⊢ ℵ Fn On
37		fvelrnb 6153	. . . . . . . . . . 11 ⊢ (ℵ Fn On → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
38	36, 37	ax-mp 5	. . . . . . . . . 10 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
39	35, 38	syl6ib 240	. . . . . . . . 9 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
40		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) = (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦)))
41	40	pwcfsdom 9284	. . . . . . . . . . 11 ⊢ (ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥)))
42		id 22	. . . . . . . . . . . 12 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
43		fveq2 6103	. . . . . . . . . . . . 13 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (cf‘(ℵ‘𝑥)) = (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
44	42, 43	oveq12d 6567	. . . . . . . . . . . 12 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥))) = ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
45	42, 44	breq12d 4596	. . . . . . . . . . 11 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑𝑚 (cf‘(ℵ‘𝑥))) ↔ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
46	41, 45	mpbii 222	. . . . . . . . . 10 ⊢ ((ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
47	46	rexlimivw 3011	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
48	39, 47	syl6 34	. . . . . . . 8 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
49	48	imp 444	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
50		ensdomtr 7981	. . . . . . 7 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≈ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ∧ (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
51	3, 49, 50	sylancr 694	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
52		fvex 6113	. . . . . . . . 9 ⊢ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V
53	52	enref 7874	. . . . . . . 8 ⊢ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))
54		mapen 8009	. . . . . . . 8 ⊢ (((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚 (ℵ‘𝐴)) ∧ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) → ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
55	2, 53, 54	mp2an 704	. . . . . . 7 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
56		cfpwsdom.1	. . . . . . . 8 ⊢ 𝐵 ∈ V
57		mapxpen 8011	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ (ℵ‘𝐴) ∈ On ∧ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V) → ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
58	56, 19, 52, 57	mp3an 1416	. . . . . . 7 ⊢ ((𝐵 ↑𝑚 (ℵ‘𝐴)) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
59	55, 58	entri 7896	. . . . . 6 ⊢ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
60		sdomentr 7979	. . . . . 6 ⊢ (((𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ∧ ((card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) ↑𝑚 (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
61	51, 59, 60	sylancl 693	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
62	4	xpdom2 7940	. . . . . . . . . 10 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)))
63	18	biimpi 205	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → ω ⊆ (ℵ‘𝐴))
64		infxpen 8720	. . . . . . . . . . 11 ⊢ (((ℵ‘𝐴) ∈ On ∧ ω ⊆ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴))
65	19, 63, 64	sylancr 694	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴))
66		domentr 7901	. . . . . . . . . 10 ⊢ ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)) ∧ ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴))
67	62, 65, 66	syl2an 493	. . . . . . . . 9 ⊢ (((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) → ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴))
68		nsuceq0 5722	. . . . . . . . . . 11 ⊢ suc 1𝑜 ≠ ∅
69		dom0 7973	. . . . . . . . . . 11 ⊢ (suc 1𝑜 ≼ ∅ ↔ suc 1𝑜 = ∅)
70	68, 69	nemtbir 2877	. . . . . . . . . 10 ⊢ ¬ suc 1𝑜 ≼ ∅
71		df-2o 7448	. . . . . . . . . . . . . 14 ⊢ 2𝑜 = suc 1𝑜
72	71	breq1i 4590	. . . . . . . . . . . . 13 ⊢ (2𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ 𝐵)
73		breq2 4587	. . . . . . . . . . . . 13 ⊢ (𝐵 = ∅ → (suc 1𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ ∅))
74	72, 73	syl5bb 271	. . . . . . . . . . . 12 ⊢ (𝐵 = ∅ → (2𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼ ∅))
75	74	biimpcd 238	. . . . . . . . . . 11 ⊢ (2𝑜 ≼ 𝐵 → (𝐵 = ∅ → suc 1𝑜 ≼ ∅))
76	75	adantld 482	. . . . . . . . . 10 ⊢ (2𝑜 ≼ 𝐵 → ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅) → suc 1𝑜 ≼ ∅))
77	70, 76	mtoi 189	. . . . . . . . 9 ⊢ (2𝑜 ≼ 𝐵 → ¬ (((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅))
78		mapdom2 8016	. . . . . . . . 9 ⊢ ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴) ∧ ¬ (((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅)) → (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
79	67, 77, 78	syl2an 493	. . . . . . . 8 ⊢ ((((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) ∧ 2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)))
80		domnsym 7971	. . . . . . . 8 ⊢ ((𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚 (ℵ‘𝐴)) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
81	79, 80	syl 17	. . . . . . 7 ⊢ ((((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ∧ 𝐴 ∈ On) ∧ 2𝑜 ≼ 𝐵) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))))
82	81	expl 646	. . . . . 6 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))))
83	82	com12 32	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ¬ (𝐵 ↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))))
84	61, 83	mt2d 130	. . . 4 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → ¬ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴))
85		domtri 9257	. . . . . 6 ⊢ (((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ∈ V ∧ (ℵ‘𝐴) ∈ V) → ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
86	52, 4, 85	mp2an 704	. . . . 5 ⊢ ((cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) ↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
87	86	biimpri 217	. . . 4 ⊢ (¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴))
88	84, 87	nsyl2 141	. . 3 ⊢ ((𝐴 ∈ On ∧ 2𝑜 ≼ 𝐵) → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))
89	88	ex 449	. 2 ⊢ (𝐴 ∈ On → (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴))))))
90		fndm 5904	. . . . . 6 ⊢ (ℵ Fn On → dom ℵ = On)
91	36, 90	ax-mp 5	. . . . 5 ⊢ dom ℵ = On
92	91	eleq2i 2680	. . . 4 ⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On)
93		ndmfv 6128	. . . 4 ⊢ (¬ 𝐴 ∈ dom ℵ → (ℵ‘𝐴) = ∅)
94	92, 93	sylnbir 320	. . 3 ⊢ (¬ 𝐴 ∈ On → (ℵ‘𝐴) = ∅)
95		1n0 7462	. . . . . 6 ⊢ 1𝑜 ≠ ∅
96		1onn 7606	. . . . . . . 8 ⊢ 1𝑜 ∈ ω
97	96	elexi 3186	. . . . . . 7 ⊢ 1𝑜 ∈ V
98	97	0sdom 7976	. . . . . 6 ⊢ (∅ ≺ 1𝑜 ↔ 1𝑜 ≠ ∅)
99	95, 98	mpbir 220	. . . . 5 ⊢ ∅ ≺ 1𝑜
100		id 22	. . . . . 6 ⊢ ((ℵ‘𝐴) = ∅ → (ℵ‘𝐴) = ∅)
101		oveq2 6557	. . . . . . . . . . 11 ⊢ ((ℵ‘𝐴) = ∅ → (𝐵 ↑𝑚 (ℵ‘𝐴)) = (𝐵 ↑𝑚 ∅))
102		map0e 7781	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → (𝐵 ↑𝑚 ∅) = 1𝑜)
103	56, 102	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐵 ↑𝑚 ∅) = 1𝑜
104	101, 103	syl6eq 2660	. . . . . . . . . 10 ⊢ ((ℵ‘𝐴) = ∅ → (𝐵 ↑𝑚 (ℵ‘𝐴)) = 1𝑜)
105	104	fveq2d 6107	. . . . . . . . 9 ⊢ ((ℵ‘𝐴) = ∅ → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) = (card‘1𝑜))
106		cardnn 8672	. . . . . . . . . 10 ⊢ (1𝑜 ∈ ω → (card‘1𝑜) = 1𝑜)
107	96, 106	ax-mp 5	. . . . . . . . 9 ⊢ (card‘1𝑜) = 1𝑜
108	105, 107	syl6eq 2660	. . . . . . . 8 ⊢ ((ℵ‘𝐴) = ∅ → (card‘(𝐵 ↑𝑚 (ℵ‘𝐴))) = 1𝑜)
109	108	fveq2d 6107	. . . . . . 7 ⊢ ((ℵ‘𝐴) = ∅ → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = (cf‘1𝑜))
110		df-1o 7447	. . . . . . . . 9 ⊢ 1𝑜 = suc ∅
111	110	fveq2i 6106	. . . . . . . 8 ⊢ (cf‘1𝑜) = (cf‘suc ∅)
112		0elon 5695	. . . . . . . . 9 ⊢ ∅ ∈ On
113		cfsuc 8962	. . . . . . . . 9 ⊢ (∅ ∈ On → (cf‘suc ∅) = 1𝑜)
114	112, 113	ax-mp 5	. . . . . . . 8 ⊢ (cf‘suc ∅) = 1𝑜
115	111, 114	eqtri 2632	. . . . . . 7 ⊢ (cf‘1𝑜) = 1𝑜
116	109, 115	syl6eq 2660	. . . . . 6 ⊢ ((ℵ‘𝐴) = ∅ → (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) = 1𝑜)
117	100, 116	breq12d 4596	. . . . 5 ⊢ ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))) ↔ ∅ ≺ 1𝑜))
118	99, 117	mpbiri 247	. . . 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 175	1 ⊢ (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚 (ℵ‘𝐴)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  dom cdm 5038  ran crn 5039  Oncon0 5640  suc csuc 5642   Fn wfn 5799  ‘cfv 5804  (class class class)co 6549  ωcom 6957  1_𝑜c1o 7440  2_𝑜c2o 7441   ↑_𝑚 cmap 7744   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840  Fincfn 7841  harchar 8344  cardccrd 8644  ℵcale 8645  cfccf 8646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-ac2 9168

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-smo 7330  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-oi 8298  df-har 8346  df-card 8648  df-aleph 8649  df-cf 8650  df-acn 8651  df-ac 8822

This theorem is referenced by:  alephom  9286