Metamath Proof Explorer

Theorem cantnflem1a

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
oemapval.t 
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
oemapval.f 
|- ( ph -> F e. S )
oemapval.g 
|- ( ph -> G e. S )
oemapvali.r 
|- ( ph -> F T G )
oemapvali.x 
|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
Assertion cantnflem1a 
|- ( ph -> X e. ( G supp (/) ) )

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 oemapval.t 
 |-  T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5 oemapval.f 
 |-  ( ph -> F e. S )
6 oemapval.g 
 |-  ( ph -> G e. S )
7 oemapvali.r 
 |-  ( ph -> F T G )
8 oemapvali.x 
 |-  X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
9 1 2 3 4 5 6 7 8 oemapvali 
 |-  ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )
10 9 simp1d 
 |-  ( ph -> X e. B )
11 9 simp2d 
 |-  ( ph -> ( F ` X ) e. ( G ` X ) )
12 11 ne0d 
 |-  ( ph -> ( G ` X ) =/= (/) )
13 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
14 6 13 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
15 14 simpld 
 |-  ( ph -> G : B --> A )
16 15 ffnd 
 |-  ( ph -> G Fn B )
17 0ex 
 |-  (/) e. _V
18 17 a1i 
 |-  ( ph -> (/) e. _V )
19 elsuppfn 
 |-  ( ( G Fn B /\ B e. On /\ (/) e. _V ) -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
20 16 3 18 19 syl3anc 
 |-  ( ph -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
21 10 12 20 mpbir2and 
 |-  ( ph -> X e. ( G supp (/) ) )