Metamath Proof Explorer

Theorem cantnflem1b

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 ) }
cantnflem1.o 
|- O = OrdIso ( _E , ( G supp (/) ) )
Assertion cantnflem1b 
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> X C_ ( O ` u ) )

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 simprr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) C_ u )
11 9 oicl 
 |-  Ord dom O
12 ovexd 
 |-  ( ph -> ( G supp (/) ) e. _V )
13 1 2 3 9 6 cantnfcl 
 |-  ( ph -> ( _E We ( G supp (/) ) /\ dom O e. _om ) )
14 13 simpld 
 |-  ( ph -> _E We ( G supp (/) ) )
15 9 oiiso 
 |-  ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
16 12 14 15 syl2anc 
 |-  ( ph -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
17 isof1o 
 |-  ( O Isom _E , _E ( dom O , ( G supp (/) ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) )
18 16 17 syl 
 |-  ( ph -> O : dom O -1-1-onto-> ( G supp (/) ) )
19 f1ocnv 
 |-  ( O : dom O -1-1-onto-> ( G supp (/) ) -> `' O : ( G supp (/) ) -1-1-onto-> dom O )
20 f1of 
 |-  ( `' O : ( G supp (/) ) -1-1-onto-> dom O -> `' O : ( G supp (/) ) --> dom O )
21 18 19 20 3syl 
 |-  ( ph -> `' O : ( G supp (/) ) --> dom O )
22 1 2 3 4 5 6 7 8 cantnflem1a 
 |-  ( ph -> X e. ( G supp (/) ) )
23 21 22 ffvelrnd 
 |-  ( ph -> ( `' O ` X ) e. dom O )
24 ordelon 
 |-  ( ( Ord dom O /\ ( `' O ` X ) e. dom O ) -> ( `' O ` X ) e. On )
25 11 23 24 sylancr 
 |-  ( ph -> ( `' O ` X ) e. On )
26 11 a1i 
 |-  ( ph -> Ord dom O )
27 ordelon 
 |-  ( ( Ord dom O /\ suc u e. dom O ) -> suc u e. On )
28 26 27 sylan 
 |-  ( ( ph /\ suc u e. dom O ) -> suc u e. On )
29 sucelon 
 |-  ( u e. On <-> suc u e. On )
30 28 29 sylibr 
 |-  ( ( ph /\ suc u e. dom O ) -> u e. On )
31 30 adantrr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> u e. On )
32 ontri1 
 |-  ( ( ( `' O ` X ) e. On /\ u e. On ) -> ( ( `' O ` X ) C_ u <-> -. u e. ( `' O ` X ) ) )
33 25 31 32 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( `' O ` X ) C_ u <-> -. u e. ( `' O ` X ) ) )
34 10 33 mpbid 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> -. u e. ( `' O ` X ) )
35 16 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
36 ordtr 
 |-  ( Ord dom O -> Tr dom O )
37 11 36 mp1i 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Tr dom O )
38 simprl 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. dom O )
39 trsuc 
 |-  ( ( Tr dom O /\ suc u e. dom O ) -> u e. dom O )
40 37 38 39 syl2anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> u e. dom O )
41 23 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) e. dom O )
42 isorel 
 |-  ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( u e. dom O /\ ( `' O ` X ) e. dom O ) ) -> ( u _E ( `' O ` X ) <-> ( O ` u ) _E ( O ` ( `' O ` X ) ) ) )
43 35 40 41 42 syl12anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u _E ( `' O ` X ) <-> ( O ` u ) _E ( O ` ( `' O ` X ) ) ) )
44 fvex 
 |-  ( `' O ` X ) e. _V
45 44 epeli 
 |-  ( u _E ( `' O ` X ) <-> u e. ( `' O ` X ) )
46 fvex 
 |-  ( O ` ( `' O ` X ) ) e. _V
47 46 epeli 
 |-  ( ( O ` u ) _E ( O ` ( `' O ` X ) ) <-> ( O ` u ) e. ( O ` ( `' O ` X ) ) )
48 43 45 47 3bitr3g 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. ( `' O ` X ) <-> ( O ` u ) e. ( O ` ( `' O ` X ) ) ) )
49 f1ocnvfv2 
 |-  ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ X e. ( G supp (/) ) ) -> ( O ` ( `' O ` X ) ) = X )
50 18 22 49 syl2anc 
 |-  ( ph -> ( O ` ( `' O ` X ) ) = X )
51 50 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` ( `' O ` X ) ) = X )
52 51 eleq2d 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( O ` u ) e. ( O ` ( `' O ` X ) ) <-> ( O ` u ) e. X ) )
53 48 52 bitrd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. ( `' O ` X ) <-> ( O ` u ) e. X ) )
54 34 53 mtbid 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> -. ( O ` u ) e. X )
55 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 ) ) ) )
56 55 simp1d 
 |-  ( ph -> X e. B )
57 onelon 
 |-  ( ( B e. On /\ X e. B ) -> X e. On )
58 3 56 57 syl2anc 
 |-  ( ph -> X e. On )
59 suppssdm 
 |-  ( G supp (/) ) C_ dom G
60 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
61 6 60 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
62 61 simpld 
 |-  ( ph -> G : B --> A )
63 59 62 fssdm 
 |-  ( ph -> ( G supp (/) ) C_ B )
64 63 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( G supp (/) ) C_ B )
65 9 oif 
 |-  O : dom O --> ( G supp (/) )
66 65 ffvelrni 
 |-  ( u e. dom O -> ( O ` u ) e. ( G supp (/) ) )
67 40 66 syl 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( G supp (/) ) )
68 64 67 sseldd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. B )
69 onelon 
 |-  ( ( B e. On /\ ( O ` u ) e. B ) -> ( O ` u ) e. On )
70 3 68 69 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. On )
71 ontri1 
 |-  ( ( X e. On /\ ( O ` u ) e. On ) -> ( X C_ ( O ` u ) <-> -. ( O ` u ) e. X ) )
72 58 70 71 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( X C_ ( O ` u ) <-> -. ( O ` u ) e. X ) )
73 54 72 mpbird 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> X C_ ( O ` u ) )