Metamath Proof Explorer

Theorem basqtop

Description: An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis qtopcmp.1 
|- X = U. J
Assertion basqtop 
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( J qTop F ) e. TopBases )

Proof

Step Hyp Ref Expression
1 qtopcmp.1 
 |-  X = U. J
2 f1ofo 
 |-  ( F : X -1-1-onto-> Y -> F : X -onto-> Y )
3 1 elqtop2 
 |-  ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( x e. ( J qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. J ) ) )
4 1 elqtop2 
 |-  ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( y e. ( J qTop F ) <-> ( y C_ Y /\ ( `' F " y ) e. J ) ) )
5 3 4 anbi12d 
 |-  ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( ( x e. ( J qTop F ) /\ y e. ( J qTop F ) ) <-> ( ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) ) )
6 2 5 sylan2 
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( x e. ( J qTop F ) /\ y e. ( J qTop F ) ) <-> ( ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) ) )
7 simpl1l 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> J e. TopBases )
8 simpl2r 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> ( `' F " x ) e. J )
9 simpl3r 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> ( `' F " y ) e. J )
10 simpl1r 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> F : X -1-1-onto-> Y )
11 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
12 f1ofn 
 |-  ( `' F : Y -1-1-onto-> X -> `' F Fn Y )
13 10 11 12 3syl 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> `' F Fn Y )
14 simpl2l 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> x C_ Y )
15 simpr 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> z e. ( x i^i y ) )
16 15 elin1d 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> z e. x )
17 fnfvima 
 |-  ( ( `' F Fn Y /\ x C_ Y /\ z e. x ) -> ( `' F ` z ) e. ( `' F " x ) )
18 13 14 16 17 syl3anc 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> ( `' F ` z ) e. ( `' F " x ) )
19 simpl3l 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> y C_ Y )
20 15 elin2d 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> z e. y )
21 fnfvima 
 |-  ( ( `' F Fn Y /\ y C_ Y /\ z e. y ) -> ( `' F ` z ) e. ( `' F " y ) )
22 13 19 20 21 syl3anc 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> ( `' F ` z ) e. ( `' F " y ) )
23 18 22 elind 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> ( `' F ` z ) e. ( ( `' F " x ) i^i ( `' F " y ) ) )
24 basis2 
 |-  ( ( ( J e. TopBases /\ ( `' F " x ) e. J ) /\ ( ( `' F " y ) e. J /\ ( `' F ` z ) e. ( ( `' F " x ) i^i ( `' F " y ) ) ) ) -> E. w e. J ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) )
25 7 8 9 23 24 syl22anc 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> E. w e. J ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) )
26 10 adantr 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> F : X -1-1-onto-> Y )
27 inss1 
 |-  ( x i^i y ) C_ x
28 simp2l 
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> x C_ Y )
29 27 28 sstrid 
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( x i^i y ) C_ Y )
30 29 sselda 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> z e. Y )
31 30 adantr 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> z e. Y )
32 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ z e. Y ) -> ( F ` ( `' F ` z ) ) = z )
33 26 31 32 syl2anc 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( F ` ( `' F ` z ) ) = z )
34 f1ofn 
 |-  ( F : X -1-1-onto-> Y -> F Fn X )
35 26 34 syl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> F Fn X )
36 simprrr 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> w C_ ( ( `' F " x ) i^i ( `' F " y ) ) )
37 inss1 
 |-  ( ( `' F " x ) i^i ( `' F " y ) ) C_ ( `' F " x )
38 36 37 sstrdi 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> w C_ ( `' F " x ) )
39 cnvimass 
 |-  ( `' F " x ) C_ dom F
40 f1odm 
 |-  ( F : X -1-1-onto-> Y -> dom F = X )
41 26 40 syl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> dom F = X )
42 39 41 sseqtrid 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( `' F " x ) C_ X )
43 38 42 sstrd 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> w C_ X )
44 simprrl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( `' F ` z ) e. w )
45 fnfvima 
 |-  ( ( F Fn X /\ w C_ X /\ ( `' F ` z ) e. w ) -> ( F ` ( `' F ` z ) ) e. ( F " w ) )
46 35 43 44 45 syl3anc 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( F ` ( `' F ` z ) ) e. ( F " w ) )
47 33 46 eqeltrrd 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> z e. ( F " w ) )
48 imassrn 
 |-  ( F " w ) C_ ran F
49 26 2 syl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> F : X -onto-> Y )
50 forn 
 |-  ( F : X -onto-> Y -> ran F = Y )
51 49 50 syl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ran F = Y )
52 48 51 sseqtrid 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( F " w ) C_ Y )
53 f1of1 
 |-  ( F : X -1-1-onto-> Y -> F : X -1-1-> Y )
54 26 53 syl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> F : X -1-1-> Y )
55 f1imacnv 
 |-  ( ( F : X -1-1-> Y /\ w C_ X ) -> ( `' F " ( F " w ) ) = w )
56 54 43 55 syl2anc 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( `' F " ( F " w ) ) = w )
57 simprl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> w e. J )
58 56 57 eqeltrd 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( `' F " ( F " w ) ) e. J )
59 7 adantr 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> J e. TopBases )
60 1 elqtop2 
 |-  ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( ( F " w ) e. ( J qTop F ) <-> ( ( F " w ) C_ Y /\ ( `' F " ( F " w ) ) e. J ) ) )
61 59 49 60 syl2anc 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( ( F " w ) e. ( J qTop F ) <-> ( ( F " w ) C_ Y /\ ( `' F " ( F " w ) ) e. J ) ) )
62 52 58 61 mpbir2and 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( F " w ) e. ( J qTop F ) )
63 fnfun 
 |-  ( F Fn X -> Fun F )
64 inpreima 
 |-  ( Fun F -> ( `' F " ( x i^i y ) ) = ( ( `' F " x ) i^i ( `' F " y ) ) )
65 35 63 64 3syl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( `' F " ( x i^i y ) ) = ( ( `' F " x ) i^i ( `' F " y ) ) )
66 36 65 sseqtrrd 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> w C_ ( `' F " ( x i^i y ) ) )
67 35 63 syl 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> Fun F )
68 38 39 sstrdi 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> w C_ dom F )
69 funimass3 
 |-  ( ( Fun F /\ w C_ dom F ) -> ( ( F " w ) C_ ( x i^i y ) <-> w C_ ( `' F " ( x i^i y ) ) ) )
70 67 68 69 syl2anc 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( ( F " w ) C_ ( x i^i y ) <-> w C_ ( `' F " ( x i^i y ) ) ) )
71 66 70 mpbird 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( F " w ) C_ ( x i^i y ) )
72 vex 
 |-  x e. _V
73 72 inex1 
 |-  ( x i^i y ) e. _V
74 73 elpw2 
 |-  ( ( F " w ) e. ~P ( x i^i y ) <-> ( F " w ) C_ ( x i^i y ) )
75 71 74 sylibr 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( F " w ) e. ~P ( x i^i y ) )
76 62 75 elind 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> ( F " w ) e. ( ( J qTop F ) i^i ~P ( x i^i y ) ) )
77 elunii 
 |-  ( ( z e. ( F " w ) /\ ( F " w ) e. ( ( J qTop F ) i^i ~P ( x i^i y ) ) ) -> z e. U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) )
78 47 76 77 syl2anc 
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) /\ ( w e. J /\ ( ( `' F ` z ) e. w /\ w C_ ( ( `' F " x ) i^i ( `' F " y ) ) ) ) ) -> z e. U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) )
79 25 78 rexlimddv 
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) /\ z e. ( x i^i y ) ) -> z e. U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) )
80 79 ex 
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( z e. ( x i^i y ) -> z e. U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) ) )
81 80 ssrdv 
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( x i^i y ) C_ U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) )
82 81 3expib 
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( ( x C_ Y /\ ( `' F " x ) e. J ) /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( x i^i y ) C_ U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) ) )
83 6 82 sylbid 
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( x e. ( J qTop F ) /\ y e. ( J qTop F ) ) -> ( x i^i y ) C_ U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) ) )
84 83 ralrimivv 
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> A. x e. ( J qTop F ) A. y e. ( J qTop F ) ( x i^i y ) C_ U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) )
85 ovex 
 |-  ( J qTop F ) e. _V
86 isbasisg 
 |-  ( ( J qTop F ) e. _V -> ( ( J qTop F ) e. TopBases <-> A. x e. ( J qTop F ) A. y e. ( J qTop F ) ( x i^i y ) C_ U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) ) )
87 85 86 ax-mp 
 |-  ( ( J qTop F ) e. TopBases <-> A. x e. ( J qTop F ) A. y e. ( J qTop F ) ( x i^i y ) C_ U. ( ( J qTop F ) i^i ~P ( x i^i y ) ) )
88 84 87 sylibr 
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( J qTop F ) e. TopBases )