Metamath Proof Explorer

Theorem cantnfresb

Description: A Cantor normal form which sums to less than a certain power has only zeros for larger components. (Contributed by RP, 3-Feb-2025)

Ref Expression
Assertion cantnfresb 
|- ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( ( ( A CNF B ) ` F ) e. ( A ^o C ) <-> A. x e. ( B \ C ) ( F ` x ) = (/) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  dom ( A CNF B ) = dom ( A CNF B )
2 eldifi 
 |-  ( A e. ( On \ 2o ) -> A e. On )
3 2 adantr 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> A e. On )
4 simpr 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> B e. On )
5 eqid 
 |-  { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } = { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) }
6 1 3 4 5 cantnf 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( A CNF B ) Isom { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } , _E ( dom ( A CNF B ) , ( A ^o B ) ) )
7 6 adantr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ F e. dom ( A CNF B ) ) -> ( A CNF B ) Isom { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } , _E ( dom ( A CNF B ) , ( A ^o B ) ) )
8 simpr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ F e. dom ( A CNF B ) ) -> F e. dom ( A CNF B ) )
9 ondif2 
 |-  ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) )
10 9 simprbi 
 |-  ( A e. ( On \ 2o ) -> 1o e. A )
11 dif20el 
 |-  ( A e. ( On \ 2o ) -> (/) e. A )
12 10 11 ifcld 
 |-  ( A e. ( On \ 2o ) -> if ( y = C , 1o , (/) ) e. A )
13 12 ad2antrr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ y e. B ) -> if ( y = C , 1o , (/) ) e. A )
14 13 fmpttd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( y e. B |-> if ( y = C , 1o , (/) ) ) : B --> A )
15 11 adantr 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> (/) e. A )
16 eqid 
 |-  ( y e. B |-> if ( y = C , 1o , (/) ) ) = ( y e. B |-> if ( y = C , 1o , (/) ) )
17 4 15 16 sniffsupp 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( y e. B |-> if ( y = C , 1o , (/) ) ) finSupp (/) )
18 1 3 4 cantnfs 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) e. dom ( A CNF B ) <-> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) : B --> A /\ ( y e. B |-> if ( y = C , 1o , (/) ) ) finSupp (/) ) ) )
19 14 17 18 mpbir2and 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( y e. B |-> if ( y = C , 1o , (/) ) ) e. dom ( A CNF B ) )
20 19 adantr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ F e. dom ( A CNF B ) ) -> ( y e. B |-> if ( y = C , 1o , (/) ) ) e. dom ( A CNF B ) )
21 isorel 
 |-  ( ( ( A CNF B ) Isom { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } , _E ( dom ( A CNF B ) , ( A ^o B ) ) /\ ( F e. dom ( A CNF B ) /\ ( y e. B |-> if ( y = C , 1o , (/) ) ) e. dom ( A CNF B ) ) ) -> ( F { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } ( y e. B |-> if ( y = C , 1o , (/) ) ) <-> ( ( A CNF B ) ` F ) _E ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) ) )
22 7 8 20 21 syl12anc 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ F e. dom ( A CNF B ) ) -> ( F { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } ( y e. B |-> if ( y = C , 1o , (/) ) ) <-> ( ( A CNF B ) ` F ) _E ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) ) )
23 22 adantrl 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( F { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } ( y e. B |-> if ( y = C , 1o , (/) ) ) <-> ( ( A CNF B ) ` F ) _E ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) ) )
24 23 adantr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ C e. B ) -> ( F { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } ( y e. B |-> if ( y = C , 1o , (/) ) ) <-> ( ( A CNF B ) ` F ) _E ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) ) )
25 fvexd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ C e. B ) -> ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) e. _V )
26 epelg 
 |-  ( ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) e. _V -> ( ( ( A CNF B ) ` F ) _E ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) <-> ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) ) )
27 25 26 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ C e. B ) -> ( ( ( A CNF B ) ` F ) _E ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) <-> ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) ) )
28 2 ad2antrr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. B ) -> A e. On )
29 simplr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. B ) -> B e. On )
30 fconst6g 
 |-  ( (/) e. A -> ( B X. { (/) } ) : B --> A )
31 11 30 syl 
 |-  ( A e. ( On \ 2o ) -> ( B X. { (/) } ) : B --> A )
32 31 adantr 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( B X. { (/) } ) : B --> A )
33 4 15 fczfsuppd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( B X. { (/) } ) finSupp (/) )
34 1 3 4 cantnfs 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( ( B X. { (/) } ) e. dom ( A CNF B ) <-> ( ( B X. { (/) } ) : B --> A /\ ( B X. { (/) } ) finSupp (/) ) ) )
35 32 33 34 mpbir2and 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( B X. { (/) } ) e. dom ( A CNF B ) )
36 35 adantr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. B ) -> ( B X. { (/) } ) e. dom ( A CNF B ) )
37 simpr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. B ) -> C e. B )
38 10 ad2antrr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. B ) -> 1o e. A )
39 fczsupp0 
 |-  ( ( B X. { (/) } ) supp (/) ) = (/)
40 0ss 
 |-  (/) C_ C
41 39 40 eqsstri 
 |-  ( ( B X. { (/) } ) supp (/) ) C_ C
42 41 a1i 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. B ) -> ( ( B X. { (/) } ) supp (/) ) C_ C )
43 0ex 
 |-  (/) e. _V
44 43 fvconst2 
 |-  ( y e. B -> ( ( B X. { (/) } ) ` y ) = (/) )
45 44 ifeq2d 
 |-  ( y e. B -> if ( y = C , 1o , ( ( B X. { (/) } ) ` y ) ) = if ( y = C , 1o , (/) ) )
46 45 mpteq2ia 
 |-  ( y e. B |-> if ( y = C , 1o , ( ( B X. { (/) } ) ` y ) ) ) = ( y e. B |-> if ( y = C , 1o , (/) ) )
47 46 eqcomi 
 |-  ( y e. B |-> if ( y = C , 1o , (/) ) ) = ( y e. B |-> if ( y = C , 1o , ( ( B X. { (/) } ) ` y ) ) )
48 1 28 29 36 37 38 42 47 cantnfp1 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. B ) -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) e. dom ( A CNF B ) /\ ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) = ( ( ( A ^o C ) .o 1o ) +o ( ( A CNF B ) ` ( B X. { (/) } ) ) ) ) )
49 48 simprd 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. B ) -> ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) = ( ( ( A ^o C ) .o 1o ) +o ( ( A CNF B ) ` ( B X. { (/) } ) ) ) )
50 49 adantrl 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ C e. B ) ) -> ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) = ( ( ( A ^o C ) .o 1o ) +o ( ( A CNF B ) ` ( B X. { (/) } ) ) ) )
51 oecl 
 |-  ( ( A e. On /\ C e. On ) -> ( A ^o C ) e. On )
52 3 51 sylan 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) -> ( A ^o C ) e. On )
53 om1 
 |-  ( ( A ^o C ) e. On -> ( ( A ^o C ) .o 1o ) = ( A ^o C ) )
54 52 53 syl 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) -> ( ( A ^o C ) .o 1o ) = ( A ^o C ) )
55 1 3 4 15 cantnf0 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = (/) )
56 55 adantr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = (/) )
57 54 56 oveq12d 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) -> ( ( ( A ^o C ) .o 1o ) +o ( ( A CNF B ) ` ( B X. { (/) } ) ) ) = ( ( A ^o C ) +o (/) ) )
58 oa0 
 |-  ( ( A ^o C ) e. On -> ( ( A ^o C ) +o (/) ) = ( A ^o C ) )
59 52 58 syl 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) -> ( ( A ^o C ) +o (/) ) = ( A ^o C ) )
60 57 59 eqtrd 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) -> ( ( ( A ^o C ) .o 1o ) +o ( ( A CNF B ) ` ( B X. { (/) } ) ) ) = ( A ^o C ) )
61 60 adantrr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ C e. B ) ) -> ( ( ( A ^o C ) .o 1o ) +o ( ( A CNF B ) ` ( B X. { (/) } ) ) ) = ( A ^o C ) )
62 50 61 eqtrd 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ C e. B ) ) -> ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) = ( A ^o C ) )
63 62 eleq2d 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ C e. B ) ) -> ( ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) <-> ( ( A CNF B ) ` F ) e. ( A ^o C ) ) )
64 63 exp32 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( C e. On -> ( C e. B -> ( ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) <-> ( ( A CNF B ) ` F ) e. ( A ^o C ) ) ) ) )
65 64 adantrd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( ( C e. On /\ F e. dom ( A CNF B ) ) -> ( C e. B -> ( ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) <-> ( ( A CNF B ) ` F ) e. ( A ^o C ) ) ) ) )
66 65 imp31 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ C e. B ) -> ( ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` ( y e. B |-> if ( y = C , 1o , (/) ) ) ) <-> ( ( A CNF B ) ` F ) e. ( A ^o C ) ) )
67 24 27 66 3bitrrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ C e. B ) -> ( ( ( A CNF B ) ` F ) e. ( A ^o C ) <-> F { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } ( y e. B |-> if ( y = C , 1o , (/) ) ) ) )
68 fveq1 
 |-  ( a = F -> ( a ` c ) = ( F ` c ) )
69 68 eleq1d 
 |-  ( a = F -> ( ( a ` c ) e. ( b ` c ) <-> ( F ` c ) e. ( b ` c ) ) )
70 fveq1 
 |-  ( a = F -> ( a ` x ) = ( F ` x ) )
71 70 eqeq1d 
 |-  ( a = F -> ( ( a ` x ) = ( b ` x ) <-> ( F ` x ) = ( b ` x ) ) )
72 71 imbi2d 
 |-  ( a = F -> ( ( c e. x -> ( a ` x ) = ( b ` x ) ) <-> ( c e. x -> ( F ` x ) = ( b ` x ) ) ) )
73 72 ralbidv 
 |-  ( a = F -> ( A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) <-> A. x e. B ( c e. x -> ( F ` x ) = ( b ` x ) ) ) )
74 69 73 anbi12d 
 |-  ( a = F -> ( ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) <-> ( ( F ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( b ` x ) ) ) ) )
75 74 rexbidv 
 |-  ( a = F -> ( E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) <-> E. c e. B ( ( F ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( b ` x ) ) ) ) )
76 fveq1 
 |-  ( b = ( y e. B |-> if ( y = C , 1o , (/) ) ) -> ( b ` c ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) )
77 76 eleq2d 
 |-  ( b = ( y e. B |-> if ( y = C , 1o , (/) ) ) -> ( ( F ` c ) e. ( b ` c ) <-> ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) ) )
78 fveq1 
 |-  ( b = ( y e. B |-> if ( y = C , 1o , (/) ) ) -> ( b ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) )
79 78 eqeq2d 
 |-  ( b = ( y e. B |-> if ( y = C , 1o , (/) ) ) -> ( ( F ` x ) = ( b ` x ) <-> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) )
80 79 imbi2d 
 |-  ( b = ( y e. B |-> if ( y = C , 1o , (/) ) ) -> ( ( c e. x -> ( F ` x ) = ( b ` x ) ) <-> ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) )
81 80 ralbidv 
 |-  ( b = ( y e. B |-> if ( y = C , 1o , (/) ) ) -> ( A. x e. B ( c e. x -> ( F ` x ) = ( b ` x ) ) <-> A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) )
82 77 81 anbi12d 
 |-  ( b = ( y e. B |-> if ( y = C , 1o , (/) ) ) -> ( ( ( F ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( b ` x ) ) ) <-> ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) ) )
83 82 rexbidv 
 |-  ( b = ( y e. B |-> if ( y = C , 1o , (/) ) ) -> ( E. c e. B ( ( F ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( b ` x ) ) ) <-> E. c e. B ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) ) )
84 75 83 5 bropabg 
 |-  ( F { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } ( y e. B |-> if ( y = C , 1o , (/) ) ) <-> ( ( F e. _V /\ ( y e. B |-> if ( y = C , 1o , (/) ) ) e. _V ) /\ E. c e. B ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) ) )
85 fveq2 
 |-  ( c = C -> ( F ` c ) = ( F ` C ) )
86 85 adantr 
 |-  ( ( c = C /\ c e. B ) -> ( F ` c ) = ( F ` C ) )
87 eqeq1 
 |-  ( y = c -> ( y = C <-> c = C ) )
88 87 ifbid 
 |-  ( y = c -> if ( y = C , 1o , (/) ) = if ( c = C , 1o , (/) ) )
89 1oex 
 |-  1o e. _V
90 89 43 ifex 
 |-  if ( c = C , 1o , (/) ) e. _V
91 88 16 90 fvmpt 
 |-  ( c e. B -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) = if ( c = C , 1o , (/) ) )
92 iftrue 
 |-  ( c = C -> if ( c = C , 1o , (/) ) = 1o )
93 91 92 sylan9eqr 
 |-  ( ( c = C /\ c e. B ) -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) = 1o )
94 86 93 eleq12d 
 |-  ( ( c = C /\ c e. B ) -> ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) <-> ( F ` C ) e. 1o ) )
95 el1o 
 |-  ( ( F ` C ) e. 1o <-> ( F ` C ) = (/) )
96 95 a1i 
 |-  ( ( c = C /\ c e. B ) -> ( ( F ` C ) e. 1o <-> ( F ` C ) = (/) ) )
97 96 biimpd 
 |-  ( ( c = C /\ c e. B ) -> ( ( F ` C ) e. 1o -> ( F ` C ) = (/) ) )
98 simpl 
 |-  ( ( c = C /\ c e. B ) -> c = C )
99 97 98 jctild 
 |-  ( ( c = C /\ c e. B ) -> ( ( F ` C ) e. 1o -> ( c = C /\ ( F ` C ) = (/) ) ) )
100 94 99 sylbid 
 |-  ( ( c = C /\ c e. B ) -> ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) -> ( c = C /\ ( F ` C ) = (/) ) ) )
101 100 expimpd 
 |-  ( c = C -> ( ( c e. B /\ ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) ) -> ( c = C /\ ( F ` C ) = (/) ) ) )
102 91 adantl 
 |-  ( ( c =/= C /\ c e. B ) -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) = if ( c = C , 1o , (/) ) )
103 simpl 
 |-  ( ( c =/= C /\ c e. B ) -> c =/= C )
104 103 neneqd 
 |-  ( ( c =/= C /\ c e. B ) -> -. c = C )
105 104 iffalsed 
 |-  ( ( c =/= C /\ c e. B ) -> if ( c = C , 1o , (/) ) = (/) )
106 102 105 eqtrd 
 |-  ( ( c =/= C /\ c e. B ) -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) = (/) )
107 106 eleq2d 
 |-  ( ( c =/= C /\ c e. B ) -> ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) <-> ( F ` c ) e. (/) ) )
108 107 biimpd 
 |-  ( ( c =/= C /\ c e. B ) -> ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) -> ( F ` c ) e. (/) ) )
109 108 expimpd 
 |-  ( c =/= C -> ( ( c e. B /\ ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) ) -> ( F ` c ) e. (/) ) )
110 noel 
 |-  -. ( F ` c ) e. (/)
111 110 pm2.21i 
 |-  ( ( F ` c ) e. (/) -> ( c = C /\ ( F ` C ) = (/) ) )
112 109 111 syl6 
 |-  ( c =/= C -> ( ( c e. B /\ ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) ) -> ( c = C /\ ( F ` C ) = (/) ) ) )
113 101 112 pm2.61ine 
 |-  ( ( c e. B /\ ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) ) -> ( c = C /\ ( F ` C ) = (/) ) )
114 113 a1i 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( ( c e. B /\ ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) ) -> ( c = C /\ ( F ` C ) = (/) ) ) )
115 fveqeq2 
 |-  ( x = C -> ( ( F ` x ) = (/) <-> ( F ` C ) = (/) ) )
116 115 ralsng 
 |-  ( C e. B -> ( A. x e. { C } ( F ` x ) = (/) <-> ( F ` C ) = (/) ) )
117 116 anbi2d 
 |-  ( C e. B -> ( ( c = C /\ A. x e. { C } ( F ` x ) = (/) ) <-> ( c = C /\ ( F ` C ) = (/) ) ) )
118 117 biimprd 
 |-  ( C e. B -> ( ( c = C /\ ( F ` C ) = (/) ) -> ( c = C /\ A. x e. { C } ( F ` x ) = (/) ) ) )
119 118 adantl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( ( c = C /\ ( F ` C ) = (/) ) -> ( c = C /\ A. x e. { C } ( F ` x ) = (/) ) ) )
120 4 anim1i 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) -> ( B e. On /\ C e. On ) )
121 120 adantr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( B e. On /\ C e. On ) )
122 pm3.31 
 |-  ( ( x e. B -> ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) -> ( ( x e. B /\ c e. x ) -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) )
123 122 a1i 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( ( x e. B -> ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) -> ( ( x e. B /\ c e. x ) -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) )
124 eldif 
 |-  ( x e. ( B \ suc C ) <-> ( x e. B /\ -. x e. suc C ) )
125 simplr 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> c = C )
126 125 eleq1d 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> ( c e. x <-> C e. x ) )
127 simpl 
 |-  ( ( B e. On /\ C e. On ) -> B e. On )
128 127 adantr 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> B e. On )
129 onelon 
 |-  ( ( B e. On /\ x e. B ) -> x e. On )
130 128 129 sylan 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> x e. On )
131 simpllr 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> C e. On )
132 ontri1 
 |-  ( ( x e. On /\ C e. On ) -> ( x C_ C <-> -. C e. x ) )
133 130 131 132 syl2anc 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> ( x C_ C <-> -. C e. x ) )
134 133 con2bid 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> ( C e. x <-> -. x C_ C ) )
135 onsssuc 
 |-  ( ( x e. On /\ C e. On ) -> ( x C_ C <-> x e. suc C ) )
136 130 131 135 syl2anc 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> ( x C_ C <-> x e. suc C ) )
137 136 notbid 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> ( -. x C_ C <-> -. x e. suc C ) )
138 126 134 137 3bitrrd 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. B ) -> ( -. x e. suc C <-> c e. x ) )
139 138 pm5.32da 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( ( x e. B /\ -. x e. suc C ) <-> ( x e. B /\ c e. x ) ) )
140 124 139 bitrid 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( x e. ( B \ suc C ) <-> ( x e. B /\ c e. x ) ) )
141 140 biimpd 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( x e. ( B \ suc C ) -> ( x e. B /\ c e. x ) ) )
142 141 imim1d 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( ( ( x e. B /\ c e. x ) -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> ( x e. ( B \ suc C ) -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) )
143 eldifi 
 |-  ( x e. ( B \ suc C ) -> x e. B )
144 143 adantl 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> x e. B )
145 eqeq1 
 |-  ( y = x -> ( y = C <-> x = C ) )
146 145 ifbid 
 |-  ( y = x -> if ( y = C , 1o , (/) ) = if ( x = C , 1o , (/) ) )
147 89 43 ifex 
 |-  if ( x = C , 1o , (/) ) e. _V
148 146 16 147 fvmpt 
 |-  ( x e. B -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) = if ( x = C , 1o , (/) ) )
149 144 148 syl 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) = if ( x = C , 1o , (/) ) )
150 128 143 129 syl2an 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> x e. On )
151 eloni 
 |-  ( x e. On -> Ord x )
152 150 151 syl 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> Ord x )
153 eloni 
 |-  ( B e. On -> Ord B )
154 153 ad2antrr 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> Ord B )
155 simplr 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> C e. On )
156 ordeldifsucon 
 |-  ( ( Ord B /\ C e. On ) -> ( x e. ( B \ suc C ) <-> ( x e. B /\ C e. x ) ) )
157 154 155 156 syl2anc 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( x e. ( B \ suc C ) <-> ( x e. B /\ C e. x ) ) )
158 157 biimpa 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> ( x e. B /\ C e. x ) )
159 ordirr 
 |-  ( Ord x -> -. x e. x )
160 eleq1 
 |-  ( x = C -> ( x e. x <-> C e. x ) )
161 160 notbid 
 |-  ( x = C -> ( -. x e. x <-> -. C e. x ) )
162 159 161 syl5ibcom 
 |-  ( Ord x -> ( x = C -> -. C e. x ) )
163 162 con2d 
 |-  ( Ord x -> ( C e. x -> -. x = C ) )
164 163 adantld 
 |-  ( Ord x -> ( ( x e. B /\ C e. x ) -> -. x = C ) )
165 152 158 164 sylc 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> -. x = C )
166 165 iffalsed 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> if ( x = C , 1o , (/) ) = (/) )
167 149 166 eqtrd 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) = (/) )
168 167 eqeq2d 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> ( ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) <-> ( F ` x ) = (/) ) )
169 168 biimpd 
 |-  ( ( ( ( B e. On /\ C e. On ) /\ c = C ) /\ x e. ( B \ suc C ) ) -> ( ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) -> ( F ` x ) = (/) ) )
170 169 ex 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( x e. ( B \ suc C ) -> ( ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) -> ( F ` x ) = (/) ) ) )
171 170 a2d 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( ( x e. ( B \ suc C ) -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> ( x e. ( B \ suc C ) -> ( F ` x ) = (/) ) ) )
172 123 142 171 3syld 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( ( x e. B -> ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) -> ( x e. ( B \ suc C ) -> ( F ` x ) = (/) ) ) )
173 172 ralimdv2 
 |-  ( ( ( B e. On /\ C e. On ) /\ c = C ) -> ( A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> A. x e. ( B \ suc C ) ( F ` x ) = (/) ) )
174 121 173 sylan 
 |-  ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) -> ( A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> A. x e. ( B \ suc C ) ( F ` x ) = (/) ) )
175 174 adantr 
 |-  ( ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) /\ A. x e. { C } ( F ` x ) = (/) ) -> ( A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> A. x e. ( B \ suc C ) ( F ` x ) = (/) ) )
176 ralun 
 |-  ( ( A. x e. { C } ( F ` x ) = (/) /\ A. x e. ( B \ suc C ) ( F ` x ) = (/) ) -> A. x e. ( { C } u. ( B \ suc C ) ) ( F ` x ) = (/) )
177 176 adantll 
 |-  ( ( ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) /\ A. x e. { C } ( F ` x ) = (/) ) /\ A. x e. ( B \ suc C ) ( F ` x ) = (/) ) -> A. x e. ( { C } u. ( B \ suc C ) ) ( F ` x ) = (/) )
178 undif3 
 |-  ( { C } u. ( B \ suc C ) ) = ( ( { C } u. B ) \ ( suc C \ { C } ) )
179 simpr 
 |-  ( ( C e. On /\ C e. B ) -> C e. B )
180 179 snssd 
 |-  ( ( C e. On /\ C e. B ) -> { C } C_ B )
181 ssequn1 
 |-  ( { C } C_ B <-> ( { C } u. B ) = B )
182 180 181 sylib 
 |-  ( ( C e. On /\ C e. B ) -> ( { C } u. B ) = B )
183 simpl 
 |-  ( ( C e. On /\ C e. B ) -> C e. On )
184 eloni 
 |-  ( C e. On -> Ord C )
185 orddif 
 |-  ( Ord C -> C = ( suc C \ { C } ) )
186 183 184 185 3syl 
 |-  ( ( C e. On /\ C e. B ) -> C = ( suc C \ { C } ) )
187 186 eqcomd 
 |-  ( ( C e. On /\ C e. B ) -> ( suc C \ { C } ) = C )
188 182 187 difeq12d 
 |-  ( ( C e. On /\ C e. B ) -> ( ( { C } u. B ) \ ( suc C \ { C } ) ) = ( B \ C ) )
189 178 188 eqtrid 
 |-  ( ( C e. On /\ C e. B ) -> ( { C } u. ( B \ suc C ) ) = ( B \ C ) )
190 189 adantll 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( { C } u. ( B \ suc C ) ) = ( B \ C ) )
191 190 adantr 
 |-  ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) -> ( { C } u. ( B \ suc C ) ) = ( B \ C ) )
192 191 raleqdv 
 |-  ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) -> ( A. x e. ( { C } u. ( B \ suc C ) ) ( F ` x ) = (/) <-> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
193 192 ad2antrr 
 |-  ( ( ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) /\ A. x e. { C } ( F ` x ) = (/) ) /\ A. x e. ( B \ suc C ) ( F ` x ) = (/) ) -> ( A. x e. ( { C } u. ( B \ suc C ) ) ( F ` x ) = (/) <-> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
194 177 193 mpbid 
 |-  ( ( ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) /\ A. x e. { C } ( F ` x ) = (/) ) /\ A. x e. ( B \ suc C ) ( F ` x ) = (/) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) )
195 194 ex 
 |-  ( ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) /\ A. x e. { C } ( F ` x ) = (/) ) -> ( A. x e. ( B \ suc C ) ( F ` x ) = (/) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
196 175 195 syld 
 |-  ( ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c = C ) /\ A. x e. { C } ( F ` x ) = (/) ) -> ( A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
197 196 expl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( ( c = C /\ A. x e. { C } ( F ` x ) = (/) ) -> ( A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) ) )
198 114 119 197 3syld 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( ( c e. B /\ ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) ) -> ( A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) ) )
199 198 expdimp 
 |-  ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c e. B ) -> ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) -> ( A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) ) )
200 199 impd 
 |-  ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) /\ c e. B ) -> ( ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
201 200 rexlimdva 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( E. c e. B ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
202 201 adantld 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( ( ( F e. _V /\ ( y e. B |-> if ( y = C , 1o , (/) ) ) e. _V ) /\ E. c e. B ( ( F ` c ) e. ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` c ) /\ A. x e. B ( c e. x -> ( F ` x ) = ( ( y e. B |-> if ( y = C , 1o , (/) ) ) ` x ) ) ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
203 84 202 biimtrid 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ C e. On ) /\ C e. B ) -> ( F { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } ( y e. B |-> if ( y = C , 1o , (/) ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
204 203 adantlrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ C e. B ) -> ( F { <. a , b >. | E. c e. B ( ( a ` c ) e. ( b ` c ) /\ A. x e. B ( c e. x -> ( a ` x ) = ( b ` x ) ) ) } ( y e. B |-> if ( y = C , 1o , (/) ) ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
205 67 204 sylbid 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ C e. B ) -> ( ( ( A CNF B ) ` F ) e. ( A ^o C ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
206 205 ex 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( C e. B -> ( ( ( A CNF B ) ` F ) e. ( A ^o C ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) ) )
207 ral0 
 |-  A. x e. (/) ( F ` x ) = (/)
208 ssdif0 
 |-  ( B C_ C <-> ( B \ C ) = (/) )
209 208 biimpi 
 |-  ( B C_ C -> ( B \ C ) = (/) )
210 209 raleqdv 
 |-  ( B C_ C -> ( A. x e. ( B \ C ) ( F ` x ) = (/) <-> A. x e. (/) ( F ` x ) = (/) ) )
211 207 210 mpbiri 
 |-  ( B C_ C -> A. x e. ( B \ C ) ( F ` x ) = (/) )
212 211 a1i13 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( B C_ C -> ( ( ( A CNF B ) ` F ) e. ( A ^o C ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) ) )
213 184 adantr 
 |-  ( ( C e. On /\ F e. dom ( A CNF B ) ) -> Ord C )
214 153 adantl 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> Ord B )
215 ordtri2or 
 |-  ( ( Ord C /\ Ord B ) -> ( C e. B \/ B C_ C ) )
216 213 214 215 syl2anr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( C e. B \/ B C_ C ) )
217 206 212 216 mpjaod 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( ( ( A CNF B ) ` F ) e. ( A ^o C ) -> A. x e. ( B \ C ) ( F ` x ) = (/) ) )
218 3 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> A e. On )
219 simpllr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> B e. On )
220 simplrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> F e. dom ( A CNF B ) )
221 15 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> (/) e. A )
222 simplrl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> C e. On )
223 1 3 4 cantnfs 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( F e. dom ( A CNF B ) <-> ( F : B --> A /\ F finSupp (/) ) ) )
224 223 biimpd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( F e. dom ( A CNF B ) -> ( F : B --> A /\ F finSupp (/) ) ) )
225 224 adantld 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( ( C e. On /\ F e. dom ( A CNF B ) ) -> ( F : B --> A /\ F finSupp (/) ) ) )
226 225 imp 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( F : B --> A /\ F finSupp (/) ) )
227 226 simpld 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> F : B --> A )
228 227 adantr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> F : B --> A )
229 fveqeq2 
 |-  ( x = y -> ( ( F ` x ) = (/) <-> ( F ` y ) = (/) ) )
230 229 rspccv 
 |-  ( A. x e. ( B \ C ) ( F ` x ) = (/) -> ( y e. ( B \ C ) -> ( F ` y ) = (/) ) )
231 230 adantl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> ( y e. ( B \ C ) -> ( F ` y ) = (/) ) )
232 231 imp 
 |-  ( ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) /\ y e. ( B \ C ) ) -> ( F ` y ) = (/) )
233 228 232 suppss 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> ( F supp (/) ) C_ C )
234 1 218 219 220 221 222 233 cantnflt2 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) /\ A. x e. ( B \ C ) ( F ` x ) = (/) ) -> ( ( A CNF B ) ` F ) e. ( A ^o C ) )
235 234 ex 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( A. x e. ( B \ C ) ( F ` x ) = (/) -> ( ( A CNF B ) ` F ) e. ( A ^o C ) ) )
236 217 235 impbid 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. On ) /\ ( C e. On /\ F e. dom ( A CNF B ) ) ) -> ( ( ( A CNF B ) ` F ) e. ( A ^o C ) <-> A. x e. ( B \ C ) ( F ` x ) = (/) ) )