This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem txpss3v

Description: A tail Cartesian product is a subset of the class of ordered triples. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Assertion txpss3v ⊢ A ⊗ B ⊆ V × V × V

Proof

Step Hyp Ref Expression
1 df-txp ⊢ A ⊗ B = 1 st ↾ V × V -1 ∘ A ∩ 2 nd ↾ V × V -1 ∘ B
2 inss1 ⊢ 1 st ↾ V × V -1 ∘ A ∩ 2 nd ↾ V × V -1 ∘ B ⊆ 1 st ↾ V × V -1 ∘ A
3 relco ⊢ Rel ⁡ 1 st ↾ V × V -1 ∘ A
4 vex ⊢ z ∈ V
5 vex ⊢ y ∈ V
6 4 5 brcnv ⊢ z 1 st ↾ V × V -1 y ↔ y 1 st ↾ V × V z
7 4 brresi ⊢ y 1 st ↾ V × V z ↔ y ∈ V × V ∧ y 1 st z
8 7 simplbi ⊢ y 1 st ↾ V × V z → y ∈ V × V
9 6 8 sylbi ⊢ z 1 st ↾ V × V -1 y → y ∈ V × V
10 9 adantl ⊢ x A z ∧ z 1 st ↾ V × V -1 y → y ∈ V × V
11 10 exlimiv ⊢ ∃ z x A z ∧ z 1 st ↾ V × V -1 y → y ∈ V × V
12 vex ⊢ x ∈ V
13 12 5 opelco ⊢ x y ∈ 1 st ↾ V × V -1 ∘ A ↔ ∃ z x A z ∧ z 1 st ↾ V × V -1 y
14 opelxp ⊢ x y ∈ V × V × V ↔ x ∈ V ∧ y ∈ V × V
15 12 14 mpbiran ⊢ x y ∈ V × V × V ↔ y ∈ V × V
16 11 13 15 3imtr4i ⊢ x y ∈ 1 st ↾ V × V -1 ∘ A → x y ∈ V × V × V
17 3 16 relssi ⊢ 1 st ↾ V × V -1 ∘ A ⊆ V × V × V
18 2 17 sstri ⊢ 1 st ↾ V × V -1 ∘ A ∩ 2 nd ↾ V × V -1 ∘ B ⊆ V × V × V
19 1 18 eqsstri ⊢ A ⊗ B ⊆ V × V × V