Step |
Hyp |
Ref |
Expression |
1 |
|
3anass |
⊢ ( ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ↔ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ) |
2 |
1
|
3exbii |
⊢ ( ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ↔ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ) |
3 |
|
exrot3 |
⊢ ( ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑢 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ) |
4 |
|
19.42v |
⊢ ( ∃ 𝑢 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ↔ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ) |
5 |
4
|
2exbii |
⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑢 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ) |
6 |
2 3 5
|
3bitri |
⊢ ( ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ) |
7 |
6
|
abbii |
⊢ { 𝑤 ∣ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) } |
8 |
|
dfrn6 |
⊢ ran ( 𝑅 ⋉ 𝑆 ) = { 𝑤 ∣ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ≠ ∅ } |
9 |
|
n0 |
⊢ ( [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ≠ ∅ ↔ ∃ 𝑢 𝑢 ∈ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ) |
10 |
|
elec1cnvxrn2 |
⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ) |
11 |
10
|
elv |
⊢ ( 𝑢 ∈ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) |
12 |
11
|
exbii |
⊢ ( ∃ 𝑢 𝑢 ∈ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) |
13 |
9 12
|
bitri |
⊢ ( [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ≠ ∅ ↔ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) |
14 |
13
|
abbii |
⊢ { 𝑤 ∣ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ≠ ∅ } = { 𝑤 ∣ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) } |
15 |
8 14
|
eqtri |
⊢ ran ( 𝑅 ⋉ 𝑆 ) = { 𝑤 ∣ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) } |
16 |
|
df-opab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) } |
17 |
7 15 16
|
3eqtr4i |
⊢ ran ( 𝑅 ⋉ 𝑆 ) = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) } |