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 ffvelrnda
 |-  ( ( 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 )