Metamath Proof Explorer

Theorem pwcfsdom

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

Ref Expression
Hypothesis pwcfsdom.1 ⊢ 𝐻 = ( 𝑦 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ↦ ( har ‘ ( 𝑓 ‘ 𝑦 ) ) )
Assertion pwcfsdom ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pwcfsdom.1 ⊢ 𝐻 = ( 𝑦 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ↦ ( har ‘ ( 𝑓 ‘ 𝑦 ) ) )
2 onzsl ⊢ ( 𝐴 ∈ On ↔ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) )
3 2 biimpi ⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) )
4 cfom ⊢ ( cf ‘ ω ) = ω
5 aleph0 ⊢ ( ℵ ‘ ∅ ) = ω
6 5 fveq2i ⊢ ( cf ‘ ( ℵ ‘ ∅ ) ) = ( cf ‘ ω )
7 4 6 5 3eqtr4i ⊢ ( cf ‘ ( ℵ ‘ ∅ ) ) = ( ℵ ‘ ∅ )
8 2fveq3 ⊢ ( 𝐴 = ∅ → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ ( ℵ ‘ ∅ ) ) )
9 fveq2 ⊢ ( 𝐴 = ∅ → ( ℵ ‘ 𝐴 ) = ( ℵ ‘ ∅ ) )
10 7 8 9 3eqtr4a ⊢ ( 𝐴 = ∅ → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) )
11 fvex ⊢ ( ℵ ‘ 𝐴 ) ∈ V
12 11 canth2 ⊢ ( ℵ ‘ 𝐴 ) ≺ 𝒫 ( ℵ ‘ 𝐴 )
13 11 pw2en ⊢ 𝒫 ( ℵ ‘ 𝐴 ) ≈ ( 2o ↑m ( ℵ ‘ 𝐴 ) )
14 sdomentr ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ 𝒫 ( ℵ ‘ 𝐴 ) ∧ 𝒫 ( ℵ ‘ 𝐴 ) ≈ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) )
15 12 13 14 mp2an ⊢ ( ℵ ‘ 𝐴 ) ≺ ( 2o ↑m ( ℵ ‘ 𝐴 ) )
16 alephon ⊢ ( ℵ ‘ 𝐴 ) ∈ On
17 alephgeom ⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )
18 omelon ⊢ ω ∈ On
19 2onn ⊢ 2o ∈ ω
20 onelss ⊢ ( ω ∈ On → ( 2o ∈ ω → 2o ⊆ ω ) )
21 18 19 20 mp2 ⊢ 2o ⊆ ω
22 sstr ⊢ ( ( 2o ⊆ ω ∧ ω ⊆ ( ℵ ‘ 𝐴 ) ) → 2o ⊆ ( ℵ ‘ 𝐴 ) )
23 21 22 mpan ⊢ ( ω ⊆ ( ℵ ‘ 𝐴 ) → 2o ⊆ ( ℵ ‘ 𝐴 ) )
24 17 23 sylbi ⊢ ( 𝐴 ∈ On → 2o ⊆ ( ℵ ‘ 𝐴 ) )
25 ssdomg ⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( 2o ⊆ ( ℵ ‘ 𝐴 ) → 2o ≼ ( ℵ ‘ 𝐴 ) ) )
26 16 24 25 mpsyl ⊢ ( 𝐴 ∈ On → 2o ≼ ( ℵ ‘ 𝐴 ) )
27 mapdom1 ⊢ ( 2o ≼ ( ℵ ‘ 𝐴 ) → ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) )
28 26 27 syl ⊢ ( 𝐴 ∈ On → ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) )
29 sdomdomtr ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ∧ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) )
30 15 28 29 sylancr ⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) )
31 oveq2 ⊢ ( ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) → ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) = ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) )
32 31 breq2d ⊢ ( ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) → ( ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ↔ ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ) )
33 30 32 syl5ibrcom ⊢ ( 𝐴 ∈ On → ( ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
34 10 33 syl5 ⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
35 alephreg ⊢ ( cf ‘ ( ℵ ‘ suc 𝑥 ) ) = ( ℵ ‘ suc 𝑥 )
36 2fveq3 ⊢ ( 𝐴 = suc 𝑥 → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ ( ℵ ‘ suc 𝑥 ) ) )
37 fveq2 ⊢ ( 𝐴 = suc 𝑥 → ( ℵ ‘ 𝐴 ) = ( ℵ ‘ suc 𝑥 ) )
38 35 36 37 3eqtr4a ⊢ ( 𝐴 = suc 𝑥 → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) )
39 38 rexlimivw ⊢ ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) )
40 39 33 syl5 ⊢ ( 𝐴 ∈ On → ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
41 cfsmo ⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ∃ 𝑓 ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
42 limelon ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ On )
43 ffn ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → 𝑓 Fn ( cf ‘ ( ℵ ‘ 𝐴 ) ) )
44 fnrnfv ⊢ ( 𝑓 Fn ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ran 𝑓 = { 𝑦 ∣ ∃ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑦 = ( 𝑓 ‘ 𝑥 ) } )
45 44 unieqd ⊢ ( 𝑓 Fn ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ∪ ran 𝑓 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑦 = ( 𝑓 ‘ 𝑥 ) } )
46 43 45 syl ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∪ ran 𝑓 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑦 = ( 𝑓 ‘ 𝑥 ) } )
47 fvex ⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
48 47 dfiun2 ⊢ ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑦 = ( 𝑓 ‘ 𝑥 ) }
49 46 48 eqtr4di ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∪ ran 𝑓 = ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) )
50 49 ad2antrl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ ran 𝑓 = ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) )
51 fnfvelrn ⊢ ( ( 𝑓 Fn ( cf ‘ ( ℵ ‘ 𝐴 ) ) ∧ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 )
52 43 51 sylan ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 )
53 sseq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑤 ) → ( 𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
54 53 rspcev ⊢ ( ( ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 )
55 52 54 sylan ⊢ ( ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 )
56 55 rexlimdva2 ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ( ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 ) )
57 56 ralimdv ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ( ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 ) )
58 57 imp ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 )
59 58 adantl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 )
60 alephislim ⊢ ( 𝐴 ∈ On ↔ Lim ( ℵ ‘ 𝐴 ) )
61 60 biimpi ⊢ ( 𝐴 ∈ On → Lim ( ℵ ‘ 𝐴 ) )
62 frn ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ran 𝑓 ⊆ ( ℵ ‘ 𝐴 ) )
63 62 adantr ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ran 𝑓 ⊆ ( ℵ ‘ 𝐴 ) )
64 coflim ⊢ ( ( Lim ( ℵ ‘ 𝐴 ) ∧ ran 𝑓 ⊆ ( ℵ ‘ 𝐴 ) ) → ( ∪ ran 𝑓 = ( ℵ ‘ 𝐴 ) ↔ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 ) )
65 61 63 64 syl2an ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ∪ ran 𝑓 = ( ℵ ‘ 𝐴 ) ↔ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 ) )
66 59 65 mpbird ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ ran 𝑓 = ( ℵ ‘ 𝐴 ) )
67 50 66 eqtr3d ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) = ( ℵ ‘ 𝐴 ) )
68 ffvelrn ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) )
69 16 oneli ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ On )
70 harcard ⊢ ( card ‘ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) )
71 iscard ⊢ ( ( card ‘ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On ∧ ∀ 𝑦 ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
72 71 simprbi ⊢ ( ( card ‘ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
73 70 72 ax-mp ⊢ ∀ 𝑦 ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) )
74 domrefg ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ( 𝑓 ‘ 𝑥 ) ≼ ( 𝑓 ‘ 𝑥 ) )
75 47 74 ax-mp ⊢ ( 𝑓 ‘ 𝑥 ) ≼ ( 𝑓 ‘ 𝑥 )
76 elharval ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ On ∧ ( 𝑓 ‘ 𝑥 ) ≼ ( 𝑓 ‘ 𝑥 ) ) )
77 76 biimpri ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ On ∧ ( 𝑓 ‘ 𝑥 ) ≼ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
78 75 77 mpan2 ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ On → ( 𝑓 ‘ 𝑥 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
79 breq1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
80 79 rspccv ⊢ ( ∀ 𝑦 ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
81 73 78 80 mpsyl ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ On → ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
82 68 69 81 3syl ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
83 harcl ⊢ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On
84 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( har ‘ ( 𝑓 ‘ 𝑦 ) ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
85 84 1 fvmptg ⊢ ( ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ∧ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On ) → ( 𝐻 ‘ 𝑥 ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
86 83 85 mpan2 ⊢ ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ( 𝐻 ‘ 𝑥 ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
87 86 breq2d ⊢ ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ( ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
88 87 adantl ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
89 82 88 mpbird ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) )
90 89 ralrimiva ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) )
91 fvex ⊢ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ∈ V
92 eqid ⊢ ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) = ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 )
93 eqid ⊢ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) = X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 )
94 91 92 93 konigth ⊢ ( ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) → ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
95 90 94 syl ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
96 95 ad2antrl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
97 67 96 eqbrtrrd ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
98 42 97 sylan ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
99 ovex ⊢ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ∈ V
100 68 ex ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) ) )
101 alephlim ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) )
102 101 eleq2d ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ) )
103 eliun ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) )
104 alephcard ⊢ ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 )
105 104 eleq2i ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) )
106 cardsdomelir ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( card ‘ ( ℵ ‘ 𝑦 ) ) → ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) )
107 105 106 sylbir ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) → ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) )
108 elharval ⊢ ( ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( ℵ ‘ 𝑦 ) ∈ On ∧ ( ℵ ‘ 𝑦 ) ≼ ( 𝑓 ‘ 𝑥 ) ) )
109 108 simprbi ⊢ ( ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ( ℵ ‘ 𝑦 ) ≼ ( 𝑓 ‘ 𝑥 ) )
110 domnsym ⊢ ( ( ℵ ‘ 𝑦 ) ≼ ( 𝑓 ‘ 𝑥 ) → ¬ ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) )
111 109 110 syl ⊢ ( ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ¬ ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) )
112 111 con2i ⊢ ( ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) → ¬ ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
113 alephon ⊢ ( ℵ ‘ 𝑦 ) ∈ On
114 ontri1 ⊢ ( ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On ∧ ( ℵ ‘ 𝑦 ) ∈ On ) → ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) ↔ ¬ ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
115 83 113 114 mp2an ⊢ ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) ↔ ¬ ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
116 112 115 sylibr ⊢ ( ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) )
117 107 116 syl ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) )
118 alephord2i ⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ 𝐴 → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) )
119 118 imp ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
120 ontr2 ⊢ ( ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On ∧ ( ℵ ‘ 𝐴 ) ∈ On ) → ( ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
121 83 16 120 mp2an ⊢ ( ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) )
122 117 119 121 syl2anr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) )
123 122 rexlimdva2 ⊢ ( 𝐴 ∈ On → ( ∃ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
124 103 123 syl5bi ⊢ ( 𝐴 ∈ On → ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
125 42 124 syl ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
126 102 125 sylbid ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
127 100 126 sylan9r ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) → ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
128 127 imp ⊢ ( ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) )
129 84 cbvmptv ⊢ ( 𝑦 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ↦ ( har ‘ ( 𝑓 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ↦ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
130 1 129 eqtri ⊢ 𝐻 = ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ↦ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
131 128 130 fmptd ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) → 𝐻 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) )
132 ffvelrn ⊢ ( ( 𝐻 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) )
133 onelss ⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( ( 𝐻 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) ) )
134 16 132 133 mpsyl ⊢ ( ( 𝐻 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) )
135 134 ralrimiva ⊢ ( 𝐻 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) )
136 ss2ixp ⊢ ( ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( ℵ ‘ 𝐴 ) )
137 91 11 ixpconst ⊢ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( ℵ ‘ 𝐴 ) = ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) )
138 136 137 sseqtrdi ⊢ ( ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
139 131 135 138 3syl ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
140 ssdomg ⊢ ( ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ∈ V → ( X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
141 99 139 140 mpsyl ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
142 141 adantrr ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
143 sdomdomtr ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ∧ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
144 98 142 143 syl2anc ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
145 144 expcom ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
146 145 3adant2 ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
147 146 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
148 16 41 147 mp2b ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
149 148 a1i ⊢ ( 𝐴 ∈ On → ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
150 34 40 149 3jaod ⊢ ( 𝐴 ∈ On → ( ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
151 3 150 mpd ⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
152 alephfnon ⊢ ℵ Fn On
153 152 fndmi ⊢ dom ℵ = On
154 153 eleq2i ⊢ ( 𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On )
155 ndmfv ⊢ ( ¬ 𝐴 ∈ dom ℵ → ( ℵ ‘ 𝐴 ) = ∅ )
156 1n0 ⊢ 1o ≠ ∅
157 1oex ⊢ 1o ∈ V
158 157 0sdom ⊢ ( ∅ ≺ 1o ↔ 1o ≠ ∅ )
159 156 158 mpbir ⊢ ∅ ≺ 1o
160 id ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( ℵ ‘ 𝐴 ) = ∅ )
161 fveq2 ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ ∅ ) )
162 cf0 ⊢ ( cf ‘ ∅ ) = ∅
163 161 162 eqtrdi ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ∅ )
164 160 163 oveq12d ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) = ( ∅ ↑m ∅ ) )
165 0ex ⊢ ∅ ∈ V
166 map0e ⊢ ( ∅ ∈ V → ( ∅ ↑m ∅ ) = 1o )
167 165 166 ax-mp ⊢ ( ∅ ↑m ∅ ) = 1o
168 164 167 eqtrdi ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) = 1o )
169 160 168 breq12d ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ↔ ∅ ≺ 1o ) )
170 159 169 mpbiri ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
171 155 170 syl ⊢ ( ¬ 𝐴 ∈ dom ℵ → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
172 154 171 sylnbir ⊢ ( ¬ 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
173 151 172 pm2.61i ⊢ ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) )