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 ( 𝐴𝐵 ) ⊆ ( V × ( V × V ) )

Proof

Step Hyp Ref Expression
1 df-txp ( 𝐴𝐵 ) = ( ( ( 1st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝐵 ) )
2 inss1 ( ( ( 1st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝐵 ) ) ⊆ ( ( 1st ↾ ( V × V ) ) ∘ 𝐴 )
3 relco Rel ( ( 1st ↾ ( V × V ) ) ∘ 𝐴 )
4 vex 𝑧 ∈ V
5 vex 𝑦 ∈ V
6 4 5 brcnv ( 𝑧 ( 1st ↾ ( V × V ) ) 𝑦𝑦 ( 1st ↾ ( V × V ) ) 𝑧 )
7 4 brresi ( 𝑦 ( 1st ↾ ( V × V ) ) 𝑧 ↔ ( 𝑦 ∈ ( V × V ) ∧ 𝑦 1st 𝑧 ) )
8 7 simplbi ( 𝑦 ( 1st ↾ ( V × V ) ) 𝑧𝑦 ∈ ( V × V ) )
9 6 8 sylbi ( 𝑧 ( 1st ↾ ( V × V ) ) 𝑦𝑦 ∈ ( V × V ) )
10 9 adantl ( ( 𝑥 𝐴 𝑧𝑧 ( 1st ↾ ( V × V ) ) 𝑦 ) → 𝑦 ∈ ( V × V ) )
11 10 exlimiv ( ∃ 𝑧 ( 𝑥 𝐴 𝑧𝑧 ( 1st ↾ ( V × V ) ) 𝑦 ) → 𝑦 ∈ ( V × V ) )
12 vex 𝑥 ∈ V
13 12 5 opelco ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 1st ↾ ( V × V ) ) ∘ 𝐴 ) ↔ ∃ 𝑧 ( 𝑥 𝐴 𝑧𝑧 ( 1st ↾ ( V × V ) ) 𝑦 ) )
14 opelxp ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × ( V × V ) ) ↔ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( V × V ) ) )
15 12 14 mpbiran ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × ( V × V ) ) ↔ 𝑦 ∈ ( V × V ) )
16 11 13 15 3imtr4i ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 1st ↾ ( V × V ) ) ∘ 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × ( V × V ) ) )
17 3 16 relssi ( ( 1st ↾ ( V × V ) ) ∘ 𝐴 ) ⊆ ( V × ( V × V ) )
18 2 17 sstri ( ( ( 1st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝐵 ) ) ⊆ ( V × ( V × V ) )
19 1 18 eqsstri ( 𝐴𝐵 ) ⊆ ( V × ( V × V ) )