Metamath Proof Explorer

Theorem cantnf2

Description: For every ordinal, A , there is a an ordinal exponent b such that A is less than ( _om ^o b ) and for every ordinal at least as large as b there is a unique Cantor normal form, f , with zeros for all the unnecessary higher terms, that sums to A . Theorem 5.3 of Schloeder p. 16. (Contributed by RP, 3-Feb-2025)

Ref Expression
Assertion cantnf2 ( 𝐴 ∈ On → ∃ 𝑏 ∈ On ∀ 𝑐 ∈ ( On ∖ 𝑏 ) ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 onexoegt ⊢ ( 𝐴 ∈ On → ∃ 𝑏 ∈ On 𝐴 ∈ ( ω ↑o 𝑏 ) )
2 eldif ⊢ ( 𝑐 ∈ ( On ∖ 𝑏 ) ↔ ( 𝑐 ∈ On ∧ ¬ 𝑐 ∈ 𝑏 ) )
3 simp2 ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) → 𝑏 ∈ On )
4 pm3.2 ⊢ ( 𝑏 ∈ On → ( 𝑐 ∈ On → ( 𝑏 ∈ On ∧ 𝑐 ∈ On ) ) )
5 3 4 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) → ( 𝑐 ∈ On → ( 𝑏 ∈ On ∧ 𝑐 ∈ On ) ) )
6 ontri1 ⊢ ( ( 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( 𝑏 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ 𝑏 ) )
7 5 6 syl6 ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) → ( 𝑐 ∈ On → ( 𝑏 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ 𝑏 ) ) )
8 7 pm5.32d ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) → ( ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ↔ ( 𝑐 ∈ On ∧ ¬ 𝑐 ∈ 𝑏 ) ) )
9 2 8 bitr4id ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) → ( 𝑐 ∈ ( On ∖ 𝑏 ) ↔ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) )
10 simplr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → 𝑎 = 𝐴 )
11 10 breq2d ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ( 𝑓 ( ω CNF 𝑐 ) 𝑎 ↔ 𝑓 ( ω CNF 𝑐 ) 𝐴 ) )
12 eqid ⊢ dom ( ω CNF 𝑐 ) = dom ( ω CNF 𝑐 )
13 omelon ⊢ ω ∈ On
14 13 a1i ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ω ∈ On )
15 simprl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → 𝑐 ∈ On )
16 15 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → 𝑐 ∈ On )
17 12 14 16 cantnff1o ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1-onto→ ( ω ↑o 𝑐 ) )
18 f1ofun ⊢ ( ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1-onto→ ( ω ↑o 𝑐 ) → Fun ( ω CNF 𝑐 ) )
19 17 18 syl ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → Fun ( ω CNF 𝑐 ) )
20 funbrfvb ⊢ ( ( Fun ( ω CNF 𝑐 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ( ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ↔ 𝑓 ( ω CNF 𝑐 ) 𝐴 ) )
21 19 20 sylancom ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ( ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ↔ 𝑓 ( ω CNF 𝑐 ) 𝐴 ) )
22 11 21 bitr4d ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ( 𝑓 ( ω CNF 𝑐 ) 𝑎 ↔ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) )
23 22 reubidva ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑎 = 𝐴 ) → ( ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) 𝑓 ( ω CNF 𝑐 ) 𝑎 ↔ ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) )
24 simpl2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → 𝑏 ∈ On )
25 13 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ω ∈ On )
26 24 15 25 3jca ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ( 𝑏 ∈ On ∧ 𝑐 ∈ On ∧ ω ∈ On ) )
27 peano1 ⊢ ∅ ∈ ω
28 26 27 jctir ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ( ( 𝑏 ∈ On ∧ 𝑐 ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) )
29 simprr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → 𝑏 ⊆ 𝑐 )
30 oewordi ⊢ ( ( ( 𝑏 ∈ On ∧ 𝑐 ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 𝑏 ⊆ 𝑐 → ( ω ↑o 𝑏 ) ⊆ ( ω ↑o 𝑐 ) ) )
31 28 29 30 sylc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ( ω ↑o 𝑏 ) ⊆ ( ω ↑o 𝑐 ) )
32 simpl3 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → 𝐴 ∈ ( ω ↑o 𝑏 ) )
33 31 32 sseldd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → 𝐴 ∈ ( ω ↑o 𝑐 ) )
34 12 25 15 cantnff1o ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1-onto→ ( ω ↑o 𝑐 ) )
35 dff1o5 ⊢ ( ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1-onto→ ( ω ↑o 𝑐 ) ↔ ( ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1→ ( ω ↑o 𝑐 ) ∧ ran ( ω CNF 𝑐 ) = ( ω ↑o 𝑐 ) ) )
36 simpr ⊢ ( ( ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1→ ( ω ↑o 𝑐 ) ∧ ran ( ω CNF 𝑐 ) = ( ω ↑o 𝑐 ) ) → ran ( ω CNF 𝑐 ) = ( ω ↑o 𝑐 ) )
37 35 36 sylbi ⊢ ( ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1-onto→ ( ω ↑o 𝑐 ) → ran ( ω CNF 𝑐 ) = ( ω ↑o 𝑐 ) )
38 34 37 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ran ( ω CNF 𝑐 ) = ( ω ↑o 𝑐 ) )
39 33 38 eleqtrrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → 𝐴 ∈ ran ( ω CNF 𝑐 ) )
40 dff1o2 ⊢ ( ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1-onto→ ( ω ↑o 𝑐 ) ↔ ( ( ω CNF 𝑐 ) Fn dom ( ω CNF 𝑐 ) ∧ Fun ◡ ( ω CNF 𝑐 ) ∧ ran ( ω CNF 𝑐 ) = ( ω ↑o 𝑐 ) ) )
41 simp2 ⊢ ( ( ( ω CNF 𝑐 ) Fn dom ( ω CNF 𝑐 ) ∧ Fun ◡ ( ω CNF 𝑐 ) ∧ ran ( ω CNF 𝑐 ) = ( ω ↑o 𝑐 ) ) → Fun ◡ ( ω CNF 𝑐 ) )
42 40 41 sylbi ⊢ ( ( ω CNF 𝑐 ) : dom ( ω CNF 𝑐 ) –1-1-onto→ ( ω ↑o 𝑐 ) → Fun ◡ ( ω CNF 𝑐 ) )
43 34 42 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → Fun ◡ ( ω CNF 𝑐 ) )
44 funcnv3 ⊢ ( Fun ◡ ( ω CNF 𝑐 ) ↔ ∀ 𝑎 ∈ ran ( ω CNF 𝑐 ) ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) 𝑓 ( ω CNF 𝑐 ) 𝑎 )
45 43 44 sylib ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ∀ 𝑎 ∈ ran ( ω CNF 𝑐 ) ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) 𝑓 ( ω CNF 𝑐 ) 𝑎 )
46 23 39 45 rspcdv2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 )
47 32 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → 𝐴 ∈ ( ω ↑o 𝑏 ) )
48 simplr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → 𝑓 ∈ dom ( ω CNF 𝑐 ) )
49 13 a1i ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ω ∈ On )
50 15 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → 𝑐 ∈ On )
51 12 49 50 cantnfs ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( 𝑓 ∈ dom ( ω CNF 𝑐 ) ↔ ( 𝑓 : 𝑐 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) )
52 48 51 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( 𝑓 : 𝑐 ⟶ ω ∧ 𝑓 finSupp ∅ ) )
53 simpr ⊢ ( ( 𝑓 : 𝑐 ⟶ ω ∧ 𝑓 finSupp ∅ ) → 𝑓 finSupp ∅ )
54 52 53 syl ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → 𝑓 finSupp ∅ )
55 eqid ⊢ dom ( ω CNF 𝑏 ) = dom ( ω CNF 𝑏 )
56 24 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → 𝑏 ∈ On )
57 29 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → 𝑏 ⊆ 𝑐 )
58 simpr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 )
59 58 47 eqeltrd ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( ω CNF 𝑐 ) ‘ 𝑓 ) ∈ ( ω ↑o 𝑏 ) )
60 1onn ⊢ 1o ∈ ω
61 ondif2 ⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
62 13 60 61 mpbir2an ⊢ ω ∈ ( On ∖ 2o )
63 62 a1i ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ω ∈ ( On ∖ 2o ) )
64 cantnfresb ⊢ ( ( ( ω ∈ ( On ∖ 2o ) ∧ 𝑐 ∈ On ) ∧ ( 𝑏 ∈ On ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ) → ( ( ( ω CNF 𝑐 ) ‘ 𝑓 ) ∈ ( ω ↑o 𝑏 ) ↔ ∀ 𝑑 ∈ ( 𝑐 ∖ 𝑏 ) ( 𝑓 ‘ 𝑑 ) = ∅ ) )
65 63 50 56 48 64 syl22anc ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( ( ω CNF 𝑐 ) ‘ 𝑓 ) ∈ ( ω ↑o 𝑏 ) ↔ ∀ 𝑑 ∈ ( 𝑐 ∖ 𝑏 ) ( 𝑓 ‘ 𝑑 ) = ∅ ) )
66 59 65 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ∀ 𝑑 ∈ ( 𝑐 ∖ 𝑏 ) ( 𝑓 ‘ 𝑑 ) = ∅ )
67 66 r19.21bi ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ ( 𝑐 ∖ 𝑏 ) ) → ( 𝑓 ‘ 𝑑 ) = ∅ )
68 27 a1i ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ∅ ∈ ω )
69 simpllr ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑓 ∈ dom ( ω CNF 𝑐 ) )
70 13 a1i ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ 𝑏 ) → ω ∈ On )
71 15 adantr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → 𝑐 ∈ On )
72 71 ad2antrr ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑐 ∈ On )
73 12 70 72 cantnfs ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑓 ∈ dom ( ω CNF 𝑐 ) ↔ ( 𝑓 : 𝑐 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) )
74 69 73 mpbid ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑓 : 𝑐 ⟶ ω ∧ 𝑓 finSupp ∅ ) )
75 74 simpld ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑓 : 𝑐 ⟶ ω )
76 57 sselda ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ 𝑏 ) → 𝑑 ∈ 𝑐 )
77 75 76 ffvelcdmd ⊢ ( ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ∧ 𝑑 ∈ 𝑏 ) → ( 𝑓 ‘ 𝑑 ) ∈ ω )
78 77 fmpttd ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) : 𝑏 ⟶ ω )
79 12 25 15 cantnfs ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ( 𝑓 ∈ dom ( ω CNF 𝑐 ) ↔ ( 𝑓 : 𝑐 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) )
80 79 simprbda ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → 𝑓 : 𝑐 ⟶ ω )
81 80 adantr ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → 𝑓 : 𝑐 ⟶ ω )
82 81 57 feqresmpt ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( 𝑓 ↾ 𝑏 ) = ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) )
83 54 68 fsuppres ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( 𝑓 ↾ 𝑏 ) finSupp ∅ )
84 82 83 eqbrtrrd ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) finSupp ∅ )
85 55 49 56 cantnfs ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) ∈ dom ( ω CNF 𝑏 ) ↔ ( ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) : 𝑏 ⟶ ω ∧ ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) finSupp ∅ ) ) )
86 78 84 85 mpbir2and ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) ∈ dom ( ω CNF 𝑏 ) )
87 55 49 56 50 57 67 68 12 86 cantnfres ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( ω CNF 𝑏 ) ‘ ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) ) = ( ( ω CNF 𝑐 ) ‘ ( 𝑑 ∈ 𝑐 ↦ ( 𝑓 ‘ 𝑑 ) ) ) )
88 82 fveq2d ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = ( ( ω CNF 𝑏 ) ‘ ( 𝑑 ∈ 𝑏 ↦ ( 𝑓 ‘ 𝑑 ) ) ) )
89 81 feqmptd ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → 𝑓 = ( 𝑑 ∈ 𝑐 ↦ ( 𝑓 ‘ 𝑑 ) ) )
90 89 fveq2d ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = ( ( ω CNF 𝑐 ) ‘ ( 𝑑 ∈ 𝑐 ↦ ( 𝑓 ‘ 𝑑 ) ) ) )
91 87 88 90 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = ( ( ω CNF 𝑐 ) ‘ 𝑓 ) )
92 91 58 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 )
93 47 54 92 3jca ⊢ ( ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) → ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ∧ ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ) )
94 93 ex ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ( ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 → ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ∧ ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ) ) )
95 94 pm4.71rd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ( ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ↔ ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ∧ ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) )
96 3an4anass ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ∧ ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ) ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ↔ ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) )
97 95 96 bitrdi ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) ∧ 𝑓 ∈ dom ( ω CNF 𝑐 ) ) → ( ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ↔ ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) ) )
98 97 reubidva ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ( ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ↔ ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) ) )
99 46 98 mpbid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) ∧ ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) ) → ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) )
100 99 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) → ( ( 𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐 ) → ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) ) )
101 9 100 sylbid ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) → ( 𝑐 ∈ ( On ∖ 𝑏 ) → ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) ) )
102 101 ralrimiv ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝑏 ) ) → ∀ 𝑐 ∈ ( On ∖ 𝑏 ) ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) )
103 102 3exp ⊢ ( 𝐴 ∈ On → ( 𝑏 ∈ On → ( 𝐴 ∈ ( ω ↑o 𝑏 ) → ∀ 𝑐 ∈ ( On ∖ 𝑏 ) ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) ) ) )
104 103 reximdvai ⊢ ( 𝐴 ∈ On → ( ∃ 𝑏 ∈ On 𝐴 ∈ ( ω ↑o 𝑏 ) → ∃ 𝑏 ∈ On ∀ 𝑐 ∈ ( On ∖ 𝑏 ) ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) ) )
105 1 104 mpd ⊢ ( 𝐴 ∈ On → ∃ 𝑏 ∈ On ∀ 𝑐 ∈ ( On ∖ 𝑏 ) ∃! 𝑓 ∈ dom ( ω CNF 𝑐 ) ( ( 𝐴 ∈ ( ω ↑o 𝑏 ) ∧ 𝑓 finSupp ∅ ) ∧ ( ( ( ω CNF 𝑏 ) ‘ ( 𝑓 ↾ 𝑏 ) ) = 𝐴 ∧ ( ( ω CNF 𝑐 ) ‘ 𝑓 ) = 𝐴 ) ) )