Metamath Proof Explorer

Theorem cantnfp1

Description: If F is created by adding a single term ( FX ) = Y to G , where X is larger than any element of the support of G , then F is also a finitely supported function and it is assigned the value ( ( A ^o X ) .o Y ) +o z where z is the value of G . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 1-Jul-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfp1.g 
|- ( ph -> G e. S )
cantnfp1.x 
|- ( ph -> X e. B )
cantnfp1.y 
|- ( ph -> Y e. A )
cantnfp1.s 
|- ( ph -> ( G supp (/) ) C_ X )
cantnfp1.f 
|- F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
Assertion cantnfp1 
|- ( ph -> ( F e. S /\ ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 cantnfp1.g 
 |-  ( ph -> G e. S )
5 cantnfp1.x 
 |-  ( ph -> X e. B )
6 cantnfp1.y 
 |-  ( ph -> Y e. A )
7 cantnfp1.s 
 |-  ( ph -> ( G supp (/) ) C_ X )
8 cantnfp1.f 
 |-  F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
9 onelon 
 |-  ( ( B e. On /\ X e. B ) -> X e. On )
10 3 5 9 syl2anc 
 |-  ( ph -> X e. On )
11 eloni 
 |-  ( X e. On -> Ord X )
12 ordirr 
 |-  ( Ord X -> -. X e. X )
13 10 11 12 3syl 
 |-  ( ph -> -. X e. X )
14 fvex 
 |-  ( G ` X ) e. _V
15 dif1o 
 |-  ( ( G ` X ) e. ( _V \ 1o ) <-> ( ( G ` X ) e. _V /\ ( G ` X ) =/= (/) ) )
16 14 15 mpbiran 
 |-  ( ( G ` X ) e. ( _V \ 1o ) <-> ( G ` X ) =/= (/) )
17 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
18 4 17 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
19 18 simpld 
 |-  ( ph -> G : B --> A )
20 19 ffnd 
 |-  ( ph -> G Fn B )
21 0ex 
 |-  (/) e. _V
22 21 a1i 
 |-  ( ph -> (/) e. _V )
23 elsuppfn 
 |-  ( ( G Fn B /\ B e. On /\ (/) e. _V ) -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
24 20 3 22 23 syl3anc 
 |-  ( ph -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
25 16 bicomi 
 |-  ( ( G ` X ) =/= (/) <-> ( G ` X ) e. ( _V \ 1o ) )
26 25 a1i 
 |-  ( ph -> ( ( G ` X ) =/= (/) <-> ( G ` X ) e. ( _V \ 1o ) ) )
27 26 anbi2d 
 |-  ( ph -> ( ( X e. B /\ ( G ` X ) =/= (/) ) <-> ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) ) )
28 24 27 bitrd 
 |-  ( ph -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) ) )
29 7 sseld 
 |-  ( ph -> ( X e. ( G supp (/) ) -> X e. X ) )
30 28 29 sylbird 
 |-  ( ph -> ( ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) -> X e. X ) )
31 5 30 mpand 
 |-  ( ph -> ( ( G ` X ) e. ( _V \ 1o ) -> X e. X ) )
32 16 31 syl5bir 
 |-  ( ph -> ( ( G ` X ) =/= (/) -> X e. X ) )
33 32 necon1bd 
 |-  ( ph -> ( -. X e. X -> ( G ` X ) = (/) ) )
34 13 33 mpd 
 |-  ( ph -> ( G ` X ) = (/) )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ Y = (/) ) /\ t e. B ) /\ t = X ) -> ( G ` X ) = (/) )
36 simpr 
 |-  ( ( ( ( ph /\ Y = (/) ) /\ t e. B ) /\ t = X ) -> t = X )
37 36 fveq2d 
 |-  ( ( ( ( ph /\ Y = (/) ) /\ t e. B ) /\ t = X ) -> ( G ` t ) = ( G ` X ) )
38 simpllr 
 |-  ( ( ( ( ph /\ Y = (/) ) /\ t e. B ) /\ t = X ) -> Y = (/) )
39 35 37 38 3eqtr4rd 
 |-  ( ( ( ( ph /\ Y = (/) ) /\ t e. B ) /\ t = X ) -> Y = ( G ` t ) )
40 eqidd 
 |-  ( ( ( ( ph /\ Y = (/) ) /\ t e. B ) /\ -. t = X ) -> ( G ` t ) = ( G ` t ) )
41 39 40 ifeqda 
 |-  ( ( ( ph /\ Y = (/) ) /\ t e. B ) -> if ( t = X , Y , ( G ` t ) ) = ( G ` t ) )
42 41 mpteq2dva 
 |-  ( ( ph /\ Y = (/) ) -> ( t e. B |-> if ( t = X , Y , ( G ` t ) ) ) = ( t e. B |-> ( G ` t ) ) )
43 8 42 syl5eq 
 |-  ( ( ph /\ Y = (/) ) -> F = ( t e. B |-> ( G ` t ) ) )
44 19 feqmptd 
 |-  ( ph -> G = ( t e. B |-> ( G ` t ) ) )
45 44 adantr 
 |-  ( ( ph /\ Y = (/) ) -> G = ( t e. B |-> ( G ` t ) ) )
46 43 45 eqtr4d 
 |-  ( ( ph /\ Y = (/) ) -> F = G )
47 4 adantr 
 |-  ( ( ph /\ Y = (/) ) -> G e. S )
48 46 47 eqeltrd 
 |-  ( ( ph /\ Y = (/) ) -> F e. S )
49 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
50 2 3 49 syl2anc 
 |-  ( ph -> ( A ^o B ) e. On )
51 1 2 3 cantnff 
 |-  ( ph -> ( A CNF B ) : S --> ( A ^o B ) )
52 51 4 ffvelrnd 
 |-  ( ph -> ( ( A CNF B ) ` G ) e. ( A ^o B ) )
53 onelon 
 |-  ( ( ( A ^o B ) e. On /\ ( ( A CNF B ) ` G ) e. ( A ^o B ) ) -> ( ( A CNF B ) ` G ) e. On )
54 50 52 53 syl2anc 
 |-  ( ph -> ( ( A CNF B ) ` G ) e. On )
55 54 adantr 
 |-  ( ( ph /\ Y = (/) ) -> ( ( A CNF B ) ` G ) e. On )
56 oa0r 
 |-  ( ( ( A CNF B ) ` G ) e. On -> ( (/) +o ( ( A CNF B ) ` G ) ) = ( ( A CNF B ) ` G ) )
57 55 56 syl 
 |-  ( ( ph /\ Y = (/) ) -> ( (/) +o ( ( A CNF B ) ` G ) ) = ( ( A CNF B ) ` G ) )
58 oveq2 
 |-  ( Y = (/) -> ( ( A ^o X ) .o Y ) = ( ( A ^o X ) .o (/) ) )
59 oecl 
 |-  ( ( A e. On /\ X e. On ) -> ( A ^o X ) e. On )
60 2 10 59 syl2anc 
 |-  ( ph -> ( A ^o X ) e. On )
61 om0 
 |-  ( ( A ^o X ) e. On -> ( ( A ^o X ) .o (/) ) = (/) )
62 60 61 syl 
 |-  ( ph -> ( ( A ^o X ) .o (/) ) = (/) )
63 58 62 sylan9eqr 
 |-  ( ( ph /\ Y = (/) ) -> ( ( A ^o X ) .o Y ) = (/) )
64 63 oveq1d 
 |-  ( ( ph /\ Y = (/) ) -> ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) = ( (/) +o ( ( A CNF B ) ` G ) ) )
65 46 fveq2d 
 |-  ( ( ph /\ Y = (/) ) -> ( ( A CNF B ) ` F ) = ( ( A CNF B ) ` G ) )
66 57 64 65 3eqtr4rd 
 |-  ( ( ph /\ Y = (/) ) -> ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )
67 48 66 jca 
 |-  ( ( ph /\ Y = (/) ) -> ( F e. S /\ ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) ) )
68 2 adantr 
 |-  ( ( ph /\ Y =/= (/) ) -> A e. On )
69 3 adantr 
 |-  ( ( ph /\ Y =/= (/) ) -> B e. On )
70 4 adantr 
 |-  ( ( ph /\ Y =/= (/) ) -> G e. S )
71 5 adantr 
 |-  ( ( ph /\ Y =/= (/) ) -> X e. B )
72 6 adantr 
 |-  ( ( ph /\ Y =/= (/) ) -> Y e. A )
73 7 adantr 
 |-  ( ( ph /\ Y =/= (/) ) -> ( G supp (/) ) C_ X )
74 1 68 69 70 71 72 73 8 cantnfp1lem1 
 |-  ( ( ph /\ Y =/= (/) ) -> F e. S )
75 onelon 
 |-  ( ( A e. On /\ Y e. A ) -> Y e. On )
76 2 6 75 syl2anc 
 |-  ( ph -> Y e. On )
77 on0eln0 
 |-  ( Y e. On -> ( (/) e. Y <-> Y =/= (/) ) )
78 76 77 syl 
 |-  ( ph -> ( (/) e. Y <-> Y =/= (/) ) )
79 78 biimpar 
 |-  ( ( ph /\ Y =/= (/) ) -> (/) e. Y )
80 eqid 
 |-  OrdIso ( _E , ( F supp (/) ) ) = OrdIso ( _E , ( F supp (/) ) )
81 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) .o ( F ` ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) .o ( F ` ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
82 eqid 
 |-  OrdIso ( _E , ( G supp (/) ) ) = OrdIso ( _E , ( G supp (/) ) )
83 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( G supp (/) ) ) ` k ) ) .o ( G ` ( OrdIso ( _E , ( G supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( G supp (/) ) ) ` k ) ) .o ( G ` ( OrdIso ( _E , ( G supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
84 1 68 69 70 71 72 73 8 79 80 81 82 83 cantnfp1lem3 
 |-  ( ( ph /\ Y =/= (/) ) -> ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )
85 74 84 jca 
 |-  ( ( ph /\ Y =/= (/) ) -> ( F e. S /\ ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) ) )
86 67 85 pm2.61dane 
 |-  ( ph -> ( F e. S /\ ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) ) )