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 limelon ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ On )
42 ffn ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → 𝑓 Fn ( cf ‘ ( ℵ ‘ 𝐴 ) ) )
43 fnrnfv ⊢ ( 𝑓 Fn ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ran 𝑓 = { 𝑦 ∣ ∃ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑦 = ( 𝑓 ‘ 𝑥 ) } )
44 43 unieqd ⊢ ( 𝑓 Fn ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ∪ ran 𝑓 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑦 = ( 𝑓 ‘ 𝑥 ) } )
45 42 44 syl ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∪ ran 𝑓 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑦 = ( 𝑓 ‘ 𝑥 ) } )
46 fvex ⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
47 46 dfiun2 ⊢ ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑦 = ( 𝑓 ‘ 𝑥 ) }
48 45 47 eqtr4di ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∪ ran 𝑓 = ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) )
49 48 ad2antrl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ ran 𝑓 = ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) )
50 fnfvelrn ⊢ ( ( 𝑓 Fn ( cf ‘ ( ℵ ‘ 𝐴 ) ) ∧ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 )
51 42 50 sylan ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 )
52 sseq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑤 ) → ( 𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
53 52 rspcev ⊢ ( ( ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 )
54 51 53 sylan ⊢ ( ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 )
55 54 rexlimdva2 ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ( ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 ) )
56 55 ralimdv ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ( ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 ) )
57 56 imp ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 )
58 57 adantl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 )
59 alephislim ⊢ ( 𝐴 ∈ On ↔ Lim ( ℵ ‘ 𝐴 ) )
60 59 biimpi ⊢ ( 𝐴 ∈ On → Lim ( ℵ ‘ 𝐴 ) )
61 frn ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ran 𝑓 ⊆ ( ℵ ‘ 𝐴 ) )
62 61 adantr ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ran 𝑓 ⊆ ( ℵ ‘ 𝐴 ) )
63 coflim ⊢ ( ( Lim ( ℵ ‘ 𝐴 ) ∧ ran 𝑓 ⊆ ( ℵ ‘ 𝐴 ) ) → ( ∪ ran 𝑓 = ( ℵ ‘ 𝐴 ) ↔ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 ) )
64 60 62 63 syl2an ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ∪ ran 𝑓 = ( ℵ ‘ 𝐴 ) ↔ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦 ) )
65 58 64 mpbird ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ ran 𝑓 = ( ℵ ‘ 𝐴 ) )
66 49 65 eqtr3d ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) = ( ℵ ‘ 𝐴 ) )
67 ffvelcdm ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) )
68 16 oneli ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ On )
69 harcard ⊢ ( card ‘ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) )
70 iscard ⊢ ( ( card ‘ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On ∧ ∀ 𝑦 ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
71 70 simprbi ⊢ ( ( card ‘ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
72 69 71 ax-mp ⊢ ∀ 𝑦 ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) )
73 domrefg ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ( 𝑓 ‘ 𝑥 ) ≼ ( 𝑓 ‘ 𝑥 ) )
74 46 73 ax-mp ⊢ ( 𝑓 ‘ 𝑥 ) ≼ ( 𝑓 ‘ 𝑥 )
75 elharval ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ On ∧ ( 𝑓 ‘ 𝑥 ) ≼ ( 𝑓 ‘ 𝑥 ) ) )
76 75 biimpri ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ On ∧ ( 𝑓 ‘ 𝑥 ) ≼ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
77 74 76 mpan2 ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ On → ( 𝑓 ‘ 𝑥 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
78 breq1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
79 78 rspccv ⊢ ( ∀ 𝑦 ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) 𝑦 ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
80 72 77 79 mpsyl ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ On → ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
81 67 68 80 3syl ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
82 harcl ⊢ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On
83 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( har ‘ ( 𝑓 ‘ 𝑦 ) ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
84 83 1 fvmptg ⊢ ( ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ∧ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On ) → ( 𝐻 ‘ 𝑥 ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
85 82 84 mpan2 ⊢ ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ( 𝐻 ‘ 𝑥 ) = ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
86 85 breq2d ⊢ ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ( ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
87 86 adantl ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ≺ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
88 81 87 mpbird ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) )
89 88 ralrimiva ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) )
90 fvex ⊢ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ∈ V
91 eqid ⊢ ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) = ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 )
92 eqid ⊢ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) = X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 )
93 90 91 92 konigth ⊢ ( ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ ( 𝐻 ‘ 𝑥 ) → ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
94 89 93 syl ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
95 94 ad2antrl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝑓 ‘ 𝑥 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
96 66 95 eqbrtrrd ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
97 41 96 sylan ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) )
98 ovex ⊢ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ∈ V
99 67 ex ⊢ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) ) )
100 alephlim ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) )
101 100 eleq2d ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ) )
102 eliun ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) )
103 alephcard ⊢ ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 )
104 103 eleq2i ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) )
105 cardsdomelir ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( card ‘ ( ℵ ‘ 𝑦 ) ) → ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) )
106 104 105 sylbir ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) → ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) )
107 elharval ⊢ ( ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( ℵ ‘ 𝑦 ) ∈ On ∧ ( ℵ ‘ 𝑦 ) ≼ ( 𝑓 ‘ 𝑥 ) ) )
108 107 simprbi ⊢ ( ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ( ℵ ‘ 𝑦 ) ≼ ( 𝑓 ‘ 𝑥 ) )
109 domnsym ⊢ ( ( ℵ ‘ 𝑦 ) ≼ ( 𝑓 ‘ 𝑥 ) → ¬ ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) )
110 108 109 syl ⊢ ( ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) → ¬ ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) )
111 110 con2i ⊢ ( ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) → ¬ ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
112 alephon ⊢ ( ℵ ‘ 𝑦 ) ∈ On
113 ontri1 ⊢ ( ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On ∧ ( ℵ ‘ 𝑦 ) ∈ On ) → ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) ↔ ¬ ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
114 82 112 113 mp2an ⊢ ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) ↔ ¬ ( ℵ ‘ 𝑦 ) ∈ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
115 111 114 sylibr ⊢ ( ( 𝑓 ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) )
116 106 115 syl ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) )
117 alephord2i ⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ 𝐴 → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) )
118 117 imp ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
119 ontr2 ⊢ ( ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ On ∧ ( ℵ ‘ 𝐴 ) ∈ On ) → ( ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
120 82 16 119 mp2an ⊢ ( ( ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ⊆ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) )
121 116 118 120 syl2anr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) )
122 121 rexlimdva2 ⊢ ( 𝐴 ∈ On → ( ∃ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
123 102 122 biimtrid ⊢ ( 𝐴 ∈ On → ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
124 41 123 syl ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
125 101 124 sylbid ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
126 99 125 sylan9r ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) → ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) ) )
127 126 imp ⊢ ( ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( har ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ℵ ‘ 𝐴 ) )
128 83 cbvmptv ⊢ ( 𝑦 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ↦ ( har ‘ ( 𝑓 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ↦ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
129 1 128 eqtri ⊢ 𝐻 = ( 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ↦ ( har ‘ ( 𝑓 ‘ 𝑥 ) ) )
130 127 129 fmptd ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) → 𝐻 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) )
131 ffvelcdm ⊢ ( ( 𝐻 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) )
132 onelss ⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( ( 𝐻 ‘ 𝑥 ) ∈ ( ℵ ‘ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) ) )
133 16 131 132 mpsyl ⊢ ( ( 𝐻 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) )
134 133 ralrimiva ⊢ ( 𝐻 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) → ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) )
135 ss2ixp ⊢ ( ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( ℵ ‘ 𝐴 ) )
136 90 11 ixpconst ⊢ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( ℵ ‘ 𝐴 ) = ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) )
137 135 136 sseqtrdi ⊢ ( ∀ 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ℵ ‘ 𝐴 ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
138 130 134 137 3syl ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
139 ssdomg ⊢ ( ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ∈ V → ( X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ⊆ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
140 98 138 139 mpsyl ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
141 140 adantrr ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
142 sdomdomtr ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ∧ X 𝑥 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) ( 𝐻 ‘ 𝑥 ) ≼ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
143 97 141 142 syl2anc ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) )
144 143 expcom ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
145 144 3adant2 ⊢ ( ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) ≺ ( ( ℵ ‘ 𝐴 ) ↑m ( cf ‘ ( ℵ ‘ 𝐴 ) ) ) ) )
146 cfsmo ⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ∃ 𝑓 ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
147 16 146 ax-mp ⊢ ∃ 𝑓 ( 𝑓 : ( cf ‘ ( ℵ ‘ 𝐴 ) ) ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑤 ∈ ( cf ‘ ( ℵ ‘ 𝐴 ) ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) )
148 145 147 exlimiiv ⊢ ( ( 𝐴 ∈ 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 ‘ ( ℵ ‘ 𝐴 ) ) )