basqtop

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

		Ref	Expression
	Hypothesis	qtopcmp.1	$⊢ X = ⋃ J$
	Assertion	basqtop	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to J qTop F \in TopBases$

Proof

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

Metamath Proof Explorer

Theorem basqtop

Proof