Metamath Proof Explorer

Theorem hsmexlem2

Description: Lemma for hsmex . Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb but use of order types allows to canonically choose the sub-bijections, removing the choice requirement. (Contributed by Stefan O'Rear, 14-Feb-2015) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses hsmexlem.f 
|- F = OrdIso ( _E , B )
hsmexlem.g 
|- G = OrdIso ( _E , U_ a e. A B )
Assertion hsmexlem2 
|- ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> dom G e. ( har ` ~P ( A X. C ) ) )

Proof

Step Hyp Ref Expression
1 hsmexlem.f 
 |-  F = OrdIso ( _E , B )
2 hsmexlem.g 
 |-  G = OrdIso ( _E , U_ a e. A B )
3 elpwi 
 |-  ( B e. ~P On -> B C_ On )
4 3 adantr 
 |-  ( ( B e. ~P On /\ dom F e. C ) -> B C_ On )
5 4 ralimi 
 |-  ( A. a e. A ( B e. ~P On /\ dom F e. C ) -> A. a e. A B C_ On )
6 iunss 
 |-  ( U_ a e. A B C_ On <-> A. a e. A B C_ On )
7 5 6 sylibr 
 |-  ( A. a e. A ( B e. ~P On /\ dom F e. C ) -> U_ a e. A B C_ On )
8 7 3ad2ant3 
 |-  ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> U_ a e. A B C_ On )
9 xpexg 
 |-  ( ( A e. V /\ C e. On ) -> ( A X. C ) e. _V )
10 9 3adant3 
 |-  ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> ( A X. C ) e. _V )
11 nfv 
 |-  F/ a C e. On
12 nfra1 
 |-  F/ a A. a e. A ( B e. ~P On /\ dom F e. C )
13 11 12 nfan 
 |-  F/ a ( C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) )
14 rsp 
 |-  ( A. a e. A ( B e. ~P On /\ dom F e. C ) -> ( a e. A -> ( B e. ~P On /\ dom F e. C ) ) )
15 onelss 
 |-  ( C e. On -> ( dom F e. C -> dom F C_ C ) )
16 15 imp 
 |-  ( ( C e. On /\ dom F e. C ) -> dom F C_ C )
17 16 adantrl 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) ) -> dom F C_ C )
18 17 3adant3 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) /\ b e. B ) -> dom F C_ C )
19 1 oismo 
 |-  ( B C_ On -> ( Smo F /\ ran F = B ) )
20 3 19 syl 
 |-  ( B e. ~P On -> ( Smo F /\ ran F = B ) )
21 20 ad2antrl 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) ) -> ( Smo F /\ ran F = B ) )
22 21 simprd 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) ) -> ran F = B )
23 1 oif 
 |-  F : dom F --> B
24 22 23 jctil 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) ) -> ( F : dom F --> B /\ ran F = B ) )
25 dffo2 
 |-  ( F : dom F -onto-> B <-> ( F : dom F --> B /\ ran F = B ) )
26 24 25 sylibr 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) ) -> F : dom F -onto-> B )
27 dffo3 
 |-  ( F : dom F -onto-> B <-> ( F : dom F --> B /\ A. b e. B E. e e. dom F b = ( F ` e ) ) )
28 27 simprbi 
 |-  ( F : dom F -onto-> B -> A. b e. B E. e e. dom F b = ( F ` e ) )
29 rsp 
 |-  ( A. b e. B E. e e. dom F b = ( F ` e ) -> ( b e. B -> E. e e. dom F b = ( F ` e ) ) )
30 26 28 29 3syl 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) ) -> ( b e. B -> E. e e. dom F b = ( F ` e ) ) )
31 30 3impia 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) /\ b e. B ) -> E. e e. dom F b = ( F ` e ) )
32 ssrexv 
 |-  ( dom F C_ C -> ( E. e e. dom F b = ( F ` e ) -> E. e e. C b = ( F ` e ) ) )
33 18 31 32 sylc 
 |-  ( ( C e. On /\ ( B e. ~P On /\ dom F e. C ) /\ b e. B ) -> E. e e. C b = ( F ` e ) )
34 33 3exp 
 |-  ( C e. On -> ( ( B e. ~P On /\ dom F e. C ) -> ( b e. B -> E. e e. C b = ( F ` e ) ) ) )
35 14 34 sylan9r 
 |-  ( ( C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> ( a e. A -> ( b e. B -> E. e e. C b = ( F ` e ) ) ) )
36 13 35 reximdai 
 |-  ( ( C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> ( E. a e. A b e. B -> E. a e. A E. e e. C b = ( F ` e ) ) )
37 36 3adant1 
 |-  ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> ( E. a e. A b e. B -> E. a e. A E. e e. C b = ( F ` e ) ) )
38 nfv 
 |-  F/ d E. e e. C b = ( F ` e )
39 nfcv 
 |-  F/_ a C
40 nfcv 
 |-  F/_ a _E
41 nfcsb1v 
 |-  F/_ a [_ d / a ]_ B
42 40 41 nfoi 
 |-  F/_ a OrdIso ( _E , [_ d / a ]_ B )
43 nfcv 
 |-  F/_ a e
44 42 43 nffv 
 |-  F/_ a ( OrdIso ( _E , [_ d / a ]_ B ) ` e )
45 44 nfeq2 
 |-  F/ a b = ( OrdIso ( _E , [_ d / a ]_ B ) ` e )
46 39 45 nfrex 
 |-  F/ a E. e e. C b = ( OrdIso ( _E , [_ d / a ]_ B ) ` e )
47 csbeq1a 
 |-  ( a = d -> B = [_ d / a ]_ B )
48 oieq2 
 |-  ( B = [_ d / a ]_ B -> OrdIso ( _E , B ) = OrdIso ( _E , [_ d / a ]_ B ) )
49 47 48 syl 
 |-  ( a = d -> OrdIso ( _E , B ) = OrdIso ( _E , [_ d / a ]_ B ) )
50 1 49 syl5eq 
 |-  ( a = d -> F = OrdIso ( _E , [_ d / a ]_ B ) )
51 50 fveq1d 
 |-  ( a = d -> ( F ` e ) = ( OrdIso ( _E , [_ d / a ]_ B ) ` e ) )
52 51 eqeq2d 
 |-  ( a = d -> ( b = ( F ` e ) <-> b = ( OrdIso ( _E , [_ d / a ]_ B ) ` e ) ) )
53 52 rexbidv 
 |-  ( a = d -> ( E. e e. C b = ( F ` e ) <-> E. e e. C b = ( OrdIso ( _E , [_ d / a ]_ B ) ` e ) ) )
54 38 46 53 cbvrexw 
 |-  ( E. a e. A E. e e. C b = ( F ` e ) <-> E. d e. A E. e e. C b = ( OrdIso ( _E , [_ d / a ]_ B ) ` e ) )
55 37 54 syl6ib 
 |-  ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> ( E. a e. A b e. B -> E. d e. A E. e e. C b = ( OrdIso ( _E , [_ d / a ]_ B ) ` e ) ) )
56 eliun 
 |-  ( b e. U_ a e. A B <-> E. a e. A b e. B )
57 vex 
 |-  d e. _V
58 vex 
 |-  e e. _V
59 57 58 op1std 
 |-  ( c = <. d , e >. -> ( 1st ` c ) = d )
60 59 csbeq1d 
 |-  ( c = <. d , e >. -> [_ ( 1st ` c ) / a ]_ B = [_ d / a ]_ B )
61 oieq2 
 |-  ( [_ ( 1st ` c ) / a ]_ B = [_ d / a ]_ B -> OrdIso ( _E , [_ ( 1st ` c ) / a ]_ B ) = OrdIso ( _E , [_ d / a ]_ B ) )
62 60 61 syl 
 |-  ( c = <. d , e >. -> OrdIso ( _E , [_ ( 1st ` c ) / a ]_ B ) = OrdIso ( _E , [_ d / a ]_ B ) )
63 57 58 op2ndd 
 |-  ( c = <. d , e >. -> ( 2nd ` c ) = e )
64 62 63 fveq12d 
 |-  ( c = <. d , e >. -> ( OrdIso ( _E , [_ ( 1st ` c ) / a ]_ B ) ` ( 2nd ` c ) ) = ( OrdIso ( _E , [_ d / a ]_ B ) ` e ) )
65 64 eqeq2d 
 |-  ( c = <. d , e >. -> ( b = ( OrdIso ( _E , [_ ( 1st ` c ) / a ]_ B ) ` ( 2nd ` c ) ) <-> b = ( OrdIso ( _E , [_ d / a ]_ B ) ` e ) ) )
66 65 rexxp 
 |-  ( E. c e. ( A X. C ) b = ( OrdIso ( _E , [_ ( 1st ` c ) / a ]_ B ) ` ( 2nd ` c ) ) <-> E. d e. A E. e e. C b = ( OrdIso ( _E , [_ d / a ]_ B ) ` e ) )
67 55 56 66 3imtr4g 
 |-  ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> ( b e. U_ a e. A B -> E. c e. ( A X. C ) b = ( OrdIso ( _E , [_ ( 1st ` c ) / a ]_ B ) ` ( 2nd ` c ) ) ) )
68 67 imp 
 |-  ( ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) /\ b e. U_ a e. A B ) -> E. c e. ( A X. C ) b = ( OrdIso ( _E , [_ ( 1st ` c ) / a ]_ B ) ` ( 2nd ` c ) ) )
69 10 68 wdomd 
 |-  ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> U_ a e. A B ~<_* ( A X. C ) )
70 2 hsmexlem1 
 |-  ( ( U_ a e. A B C_ On /\ U_ a e. A B ~<_* ( A X. C ) ) -> dom G e. ( har ` ~P ( A X. C ) ) )
71 8 69 70 syl2anc 
 |-  ( ( A e. V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> dom G e. ( har ` ~P ( A X. C ) ) )