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 ) )