Metamath Proof Explorer

Theorem cantnfp1lem1

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 20-Jun-2015) (Revised by AV, 30-Jun-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 cantnfp1lem1 
|- ( ph -> F e. S )

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 6 adantr 
 |-  ( ( ph /\ t e. B ) -> Y e. A )
10 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
11 4 10 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
12 11 simpld 
 |-  ( ph -> G : B --> A )
13 12 ffvelcdmda 
 |-  ( ( ph /\ t e. B ) -> ( G ` t ) e. A )
14 9 13 ifcld 
 |-  ( ( ph /\ t e. B ) -> if ( t = X , Y , ( G ` t ) ) e. A )
15 14 8 fmptd 
 |-  ( ph -> F : B --> A )
16 11 simprd 
 |-  ( ph -> G finSupp (/) )
17 16 fsuppimpd 
 |-  ( ph -> ( G supp (/) ) e. Fin )
18 snfi 
 |-  { X } e. Fin
19 unfi 
 |-  ( ( ( G supp (/) ) e. Fin /\ { X } e. Fin ) -> ( ( G supp (/) ) u. { X } ) e. Fin )
20 17 18 19 sylancl 
 |-  ( ph -> ( ( G supp (/) ) u. { X } ) e. Fin )
21 eqeq1 
 |-  ( t = k -> ( t = X <-> k = X ) )
22 fveq2 
 |-  ( t = k -> ( G ` t ) = ( G ` k ) )
23 21 22 ifbieq2d 
 |-  ( t = k -> if ( t = X , Y , ( G ` t ) ) = if ( k = X , Y , ( G ` k ) ) )
24 eldifi 
 |-  ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> k e. B )
25 24 adantl 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> k e. B )
26 6 adantr 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> Y e. A )
27 fvex 
 |-  ( G ` k ) e. _V
28 ifexg 
 |-  ( ( Y e. A /\ ( G ` k ) e. _V ) -> if ( k = X , Y , ( G ` k ) ) e. _V )
29 26 27 28 sylancl 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> if ( k = X , Y , ( G ` k ) ) e. _V )
30 8 23 25 29 fvmptd3 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( F ` k ) = if ( k = X , Y , ( G ` k ) ) )
31 eldifn 
 |-  ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> -. k e. ( ( G supp (/) ) u. { X } ) )
32 31 adantl 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> -. k e. ( ( G supp (/) ) u. { X } ) )
33 velsn 
 |-  ( k e. { X } <-> k = X )
34 elun2 
 |-  ( k e. { X } -> k e. ( ( G supp (/) ) u. { X } ) )
35 33 34 sylbir 
 |-  ( k = X -> k e. ( ( G supp (/) ) u. { X } ) )
36 32 35 nsyl 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> -. k = X )
37 36 iffalsed 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> if ( k = X , Y , ( G ` k ) ) = ( G ` k ) )
38 ssun1 
 |-  ( G supp (/) ) C_ ( ( G supp (/) ) u. { X } )
39 sscon 
 |-  ( ( G supp (/) ) C_ ( ( G supp (/) ) u. { X } ) -> ( B \ ( ( G supp (/) ) u. { X } ) ) C_ ( B \ ( G supp (/) ) ) )
40 38 39 ax-mp 
 |-  ( B \ ( ( G supp (/) ) u. { X } ) ) C_ ( B \ ( G supp (/) ) )
41 40 sseli 
 |-  ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> k e. ( B \ ( G supp (/) ) ) )
42 ssidd 
 |-  ( ph -> ( G supp (/) ) C_ ( G supp (/) ) )
43 0ex 
 |-  (/) e. _V
44 43 a1i 
 |-  ( ph -> (/) e. _V )
45 12 42 3 44 suppssr 
 |-  ( ( ph /\ k e. ( B \ ( G supp (/) ) ) ) -> ( G ` k ) = (/) )
46 41 45 sylan2 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( G ` k ) = (/) )
47 30 37 46 3eqtrd 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( F ` k ) = (/) )
48 15 47 suppss 
 |-  ( ph -> ( F supp (/) ) C_ ( ( G supp (/) ) u. { X } ) )
49 20 48 ssfid 
 |-  ( ph -> ( F supp (/) ) e. Fin )
50 8 funmpt2 
 |-  Fun F
51 mptexg 
 |-  ( B e. On -> ( t e. B |-> if ( t = X , Y , ( G ` t ) ) ) e. _V )
52 8 51 eqeltrid 
 |-  ( B e. On -> F e. _V )
53 3 52 syl 
 |-  ( ph -> F e. _V )
54 funisfsupp 
 |-  ( ( Fun F /\ F e. _V /\ (/) e. _V ) -> ( F finSupp (/) <-> ( F supp (/) ) e. Fin ) )
55 50 53 44 54 mp3an2i 
 |-  ( ph -> ( F finSupp (/) <-> ( F supp (/) ) e. Fin ) )
56 49 55 mpbird 
 |-  ( ph -> F finSupp (/) )
57 1 2 3 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )
58 15 56 57 mpbir2and 
 |-  ( ph -> F e. S )