Step |
Hyp |
Ref |
Expression |
1 |
|
xpord2.1 |
⊢ 𝑇 = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } |
2 |
|
opex |
⊢ 〈 𝑎 , 𝑏 〉 ∈ V |
3 |
|
opex |
⊢ 〈 𝑐 , 𝑑 〉 ∈ V |
4 |
|
eleq1 |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ 〈 𝑎 , 𝑏 〉 ∈ ( 𝐴 × 𝐵 ) ) ) |
5 |
|
opelxp |
⊢ ( 〈 𝑎 , 𝑏 〉 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) |
6 |
4 5
|
bitrdi |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ) |
7 |
|
vex |
⊢ 𝑎 ∈ V |
8 |
|
vex |
⊢ 𝑏 ∈ V |
9 |
7 8
|
op1std |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( 1st ‘ 𝑥 ) = 𝑎 ) |
10 |
9
|
breq1d |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ↔ 𝑎 𝑅 ( 1st ‘ 𝑦 ) ) ) |
11 |
9
|
eqeq1d |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ↔ 𝑎 = ( 1st ‘ 𝑦 ) ) ) |
12 |
10 11
|
orbi12d |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ↔ ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ) ) |
13 |
7 8
|
op2ndd |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( 2nd ‘ 𝑥 ) = 𝑏 ) |
14 |
13
|
breq1d |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ↔ 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ) ) |
15 |
13
|
eqeq1d |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ↔ 𝑏 = ( 2nd ‘ 𝑦 ) ) ) |
16 |
14 15
|
orbi12d |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ↔ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ) ) |
17 |
|
neeq1 |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( 𝑥 ≠ 𝑦 ↔ 〈 𝑎 , 𝑏 〉 ≠ 𝑦 ) ) |
18 |
12 16 17
|
3anbi123d |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ∧ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ∧ 〈 𝑎 , 𝑏 〉 ≠ 𝑦 ) ) ) |
19 |
6 18
|
3anbi13d |
⊢ ( 𝑥 = 〈 𝑎 , 𝑏 〉 → ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ∧ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ∧ 〈 𝑎 , 𝑏 〉 ≠ 𝑦 ) ) ) ) |
20 |
|
eleq1 |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 𝑦 ∈ ( 𝐴 × 𝐵 ) ↔ 〈 𝑐 , 𝑑 〉 ∈ ( 𝐴 × 𝐵 ) ) ) |
21 |
|
opelxp |
⊢ ( 〈 𝑐 , 𝑑 〉 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) |
22 |
20 21
|
bitrdi |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 𝑦 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ) |
23 |
|
vex |
⊢ 𝑐 ∈ V |
24 |
|
vex |
⊢ 𝑑 ∈ V |
25 |
23 24
|
op1std |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 1st ‘ 𝑦 ) = 𝑐 ) |
26 |
25
|
breq2d |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ↔ 𝑎 𝑅 𝑐 ) ) |
27 |
25
|
eqeq2d |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 𝑎 = ( 1st ‘ 𝑦 ) ↔ 𝑎 = 𝑐 ) ) |
28 |
26 27
|
orbi12d |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ↔ ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ) ) ) |
29 |
23 24
|
op2ndd |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 2nd ‘ 𝑦 ) = 𝑑 ) |
30 |
29
|
breq2d |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ↔ 𝑏 𝑆 𝑑 ) ) |
31 |
29
|
eqeq2d |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 𝑏 = ( 2nd ‘ 𝑦 ) ↔ 𝑏 = 𝑑 ) ) |
32 |
30 31
|
orbi12d |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ↔ ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ) ) ) |
33 |
|
neeq2 |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 〈 𝑎 , 𝑏 〉 ≠ 𝑦 ↔ 〈 𝑎 , 𝑏 〉 ≠ 〈 𝑐 , 𝑑 〉 ) ) |
34 |
7 8
|
opthne |
⊢ ( 〈 𝑎 , 𝑏 〉 ≠ 〈 𝑐 , 𝑑 〉 ↔ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) |
35 |
33 34
|
bitrdi |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( 〈 𝑎 , 𝑏 〉 ≠ 𝑦 ↔ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) ) |
36 |
28 32 35
|
3anbi123d |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ∧ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ∧ 〈 𝑎 , 𝑏 〉 ≠ 𝑦 ) ↔ ( ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ) ∧ ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ) ∧ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) ) ) |
37 |
22 36
|
3anbi23d |
⊢ ( 𝑦 = 〈 𝑐 , 𝑑 〉 → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ∧ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ∧ 〈 𝑎 , 𝑏 〉 ≠ 𝑦 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ) ∧ ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ) ∧ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) ) ) ) |
38 |
2 3 19 37 1
|
brab |
⊢ ( 〈 𝑎 , 𝑏 〉 𝑇 〈 𝑐 , 𝑑 〉 ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ) ∧ ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ) ∧ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) ) ) |