Metamath Proof Explorer

Theorem cantnflem1c

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

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 ) }
cantnflem1.o 
|- O = OrdIso ( _E , ( G supp (/) ) )
Assertion cantnflem1c 
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> 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 cantnflem1.o 
 |-  O = OrdIso ( _E , ( G supp (/) ) )
10 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> B e. On )
11 simplr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. B )
12 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
13 6 12 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
14 13 simpld 
 |-  ( ph -> G : B --> A )
15 14 ffnd 
 |-  ( ph -> G Fn B )
16 15 ad3antrrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> G Fn B )
17 1 2 3 4 5 6 7 8 9 cantnflem1b 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> X C_ ( O ` u ) )
18 17 ad2antrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> X C_ ( O ` u ) )
19 simprr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. x )
20 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 ) ) ) )
21 20 simp1d 
 |-  ( ph -> X e. B )
22 onelon 
 |-  ( ( B e. On /\ X e. B ) -> X e. On )
23 3 21 22 syl2anc 
 |-  ( ph -> X e. On )
24 23 ad3antrrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> X e. On )
25 onss 
 |-  ( B e. On -> B C_ On )
26 3 25 syl 
 |-  ( ph -> B C_ On )
27 26 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. On )
28 27 ad4ant13 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. On )
29 ontr2 
 |-  ( ( X e. On /\ x e. On ) -> ( ( X C_ ( O ` u ) /\ ( O ` u ) e. x ) -> X e. x ) )
30 24 28 29 syl2anc 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( X C_ ( O ` u ) /\ ( O ` u ) e. x ) -> X e. x ) )
31 18 19 30 mp2and 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> X e. x )
32 eleq2w 
 |-  ( w = x -> ( X e. w <-> X e. x ) )
33 fveq2 
 |-  ( w = x -> ( F ` w ) = ( F ` x ) )
34 fveq2 
 |-  ( w = x -> ( G ` w ) = ( G ` x ) )
35 33 34 eqeq12d 
 |-  ( w = x -> ( ( F ` w ) = ( G ` w ) <-> ( F ` x ) = ( G ` x ) ) )
36 32 35 imbi12d 
 |-  ( w = x -> ( ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> ( X e. x -> ( F ` x ) = ( G ` x ) ) ) )
37 20 simp3d 
 |-  ( ph -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
38 37 ad3antrrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
39 36 38 11 rspcdva 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( X e. x -> ( F ` x ) = ( G ` x ) ) )
40 31 39 mpd 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( F ` x ) = ( G ` x ) )
41 simprl 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( F ` x ) =/= (/) )
42 40 41 eqnetrrd 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( G ` x ) =/= (/) )
43 fvn0elsupp 
 |-  ( ( ( B e. On /\ x e. B ) /\ ( G Fn B /\ ( G ` x ) =/= (/) ) ) -> x e. ( G supp (/) ) )
44 10 11 16 42 43 syl22anc 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. ( G supp (/) ) )