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

Metamath Proof Explorer

Theorem rnxrn

Description: Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020)

Ref Expression
Assertion rnxrn ⊢ ran ⁡ R ⋉ S = x y | ∃ u u R x ∧ u S y

Proof

Step Hyp Ref Expression
1 3anass ⊢ w = x y ∧ u R x ∧ u S y ↔ w = x y ∧ u R x ∧ u S y
2 1 3exbii ⊢ ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y ↔ ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y
3 exrot3 ⊢ ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y ↔ ∃ x ∃ y ∃ u w = x y ∧ u R x ∧ u S y
4 19.42v ⊢ ∃ u w = x y ∧ u R x ∧ u S y ↔ w = x y ∧ ∃ u u R x ∧ u S y
5 4 2exbii ⊢ ∃ x ∃ y ∃ u w = x y ∧ u R x ∧ u S y ↔ ∃ x ∃ y w = x y ∧ ∃ u u R x ∧ u S y
6 2 3 5 3bitri ⊢ ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y ↔ ∃ x ∃ y w = x y ∧ ∃ u u R x ∧ u S y
7 6 abbii ⊢ w | ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y = w | ∃ x ∃ y w = x y ∧ ∃ u u R x ∧ u S y
8 dfrn6 ⊢ ran ⁡ R ⋉ S = w | w R ⋉ S -1 ≠ ∅
9 n0 ⊢ w R ⋉ S -1 ≠ ∅ ↔ ∃ u u ∈ w R ⋉ S -1
10 elec1cnvxrn2 ⊢ u ∈ V → u ∈ w R ⋉ S -1 ↔ ∃ x ∃ y w = x y ∧ u R x ∧ u S y
11 10 elv ⊢ u ∈ w R ⋉ S -1 ↔ ∃ x ∃ y w = x y ∧ u R x ∧ u S y
12 11 exbii ⊢ ∃ u u ∈ w R ⋉ S -1 ↔ ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y
13 9 12 bitri ⊢ w R ⋉ S -1 ≠ ∅ ↔ ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y
14 13 abbii ⊢ w | w R ⋉ S -1 ≠ ∅ = w | ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y
15 8 14 eqtri ⊢ ran ⁡ R ⋉ S = w | ∃ u ∃ x ∃ y w = x y ∧ u R x ∧ u S y
16 df-opab ⊢ x y | ∃ u u R x ∧ u S y = w | ∃ x ∃ y w = x y ∧ ∃ u u R x ∧ u S y
17 7 15 16 3eqtr4i ⊢ ran ⁡ R ⋉ S = x y | ∃ u u R x ∧ u S y