txss12

Description: Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	txss12	$⊢ ((B \in V \land D \in W) \land (A \subseteq B \land C \subseteq D)) \to A \times_{t} C \subseteq B \times_{t} D$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran (x \in B, y \in D ⟼ x \times y) = ran (x \in B, y \in D ⟼ x \times y)$
2	1	txbasex	$⊢ (B \in V \land D \in W) \to ran (x \in B, y \in D ⟼ x \times y) \in V$
3		resmpo	$⊢ (A \subseteq B \land C \subseteq D) \to {(x \in B, y \in D ⟼ x \times y) ↾}_{(A \times C)} = (x \in A, y \in C ⟼ x \times y)$
4		resss	$⊢ {(x \in B, y \in D ⟼ x \times y) ↾}_{(A \times C)} \subseteq (x \in B, y \in D ⟼ x \times y)$
5	3 4	eqsstrrdi	$⊢ (A \subseteq B \land C \subseteq D) \to (x \in A, y \in C ⟼ x \times y) \subseteq (x \in B, y \in D ⟼ x \times y)$
6	5	adantl	$⊢ ((B \in V \land D \in W) \land (A \subseteq B \land C \subseteq D)) \to (x \in A, y \in C ⟼ x \times y) \subseteq (x \in B, y \in D ⟼ x \times y)$
7		rnss	$⊢ (x \in A, y \in C ⟼ x \times y) \subseteq (x \in B, y \in D ⟼ x \times y) \to ran (x \in A, y \in C ⟼ x \times y) \subseteq ran (x \in B, y \in D ⟼ x \times y)$
8	6 7	syl	$⊢ ((B \in V \land D \in W) \land (A \subseteq B \land C \subseteq D)) \to ran (x \in A, y \in C ⟼ x \times y) \subseteq ran (x \in B, y \in D ⟼ x \times y)$
9		tgss	$⊢ (ran (x \in B, y \in D ⟼ x \times y) \in V \land ran (x \in A, y \in C ⟼ x \times y) \subseteq ran (x \in B, y \in D ⟼ x \times y)) \to topGen (ran (x \in A, y \in C ⟼ x \times y)) \subseteq topGen (ran (x \in B, y \in D ⟼ x \times y))$
10	2 8 9	syl2an2r	$⊢ ((B \in V \land D \in W) \land (A \subseteq B \land C \subseteq D)) \to topGen (ran (x \in A, y \in C ⟼ x \times y)) \subseteq topGen (ran (x \in B, y \in D ⟼ x \times y))$
11		ssexg	$⊢ (A \subseteq B \land B \in V) \to A \in V$
12		ssexg	$⊢ (C \subseteq D \land D \in W) \to C \in V$
13		eqid	$⊢ ran (x \in A, y \in C ⟼ x \times y) = ran (x \in A, y \in C ⟼ x \times y)$
14	13	txval	$⊢ (A \in V \land C \in V) \to A \times_{t} C = topGen (ran (x \in A, y \in C ⟼ x \times y))$
15	11 12 14	syl2an	$⊢ ((A \subseteq B \land B \in V) \land (C \subseteq D \land D \in W)) \to A \times_{t} C = topGen (ran (x \in A, y \in C ⟼ x \times y))$
16	15	an4s	$⊢ ((A \subseteq B \land C \subseteq D) \land (B \in V \land D \in W)) \to A \times_{t} C = topGen (ran (x \in A, y \in C ⟼ x \times y))$
17	16	ancoms	$⊢ ((B \in V \land D \in W) \land (A \subseteq B \land C \subseteq D)) \to A \times_{t} C = topGen (ran (x \in A, y \in C ⟼ x \times y))$
18	1	txval	$⊢ (B \in V \land D \in W) \to B \times_{t} D = topGen (ran (x \in B, y \in D ⟼ x \times y))$
19	18	adantr	$⊢ ((B \in V \land D \in W) \land (A \subseteq B \land C \subseteq D)) \to B \times_{t} D = topGen (ran (x \in B, y \in D ⟼ x \times y))$
20	10 17 19	3sstr4d	$⊢ ((B \in V \land D \in W) \land (A \subseteq B \land C \subseteq D)) \to A \times_{t} C \subseteq B \times_{t} D$

Metamath Proof Explorer

Theorem txss12

Proof