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

Metamath Proof Explorer

Theorem xrnss3v

Description: A range Cartesian product is a subset of the class of ordered triples. This is Scott Fenton's txpss3v with a different symbol, see https://github.com/metamath/set.mm/issues/2469 . (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Assertion xrnss3v ( 𝐴 ⋉ 𝐵 ) ⊆ ( V × ( V × V ) )

Proof

Step Hyp Ref Expression
1 df-xrn ⊢ ( 𝐴 ⋉ 𝐵 ) = ( ( ◡ ( 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 ) )