Step |
Hyp |
Ref |
Expression |
1 |
|
df-pred |
⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) |
2 |
1
|
elin2 |
⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) ) |
3 |
2
|
baib |
⊢ ( 𝑌 ∈ 𝐴 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) ) |
4 |
3
|
adantl |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) ) |
5 |
|
elimasng |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ 〈 𝑋 , 𝑌 〉 ∈ ◡ 𝑅 ) ) |
6 |
|
df-br |
⊢ ( 𝑋 ◡ 𝑅 𝑌 ↔ 〈 𝑋 , 𝑌 〉 ∈ ◡ 𝑅 ) |
7 |
5 6
|
bitr4di |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ 𝑋 ◡ 𝑅 𝑌 ) ) |
8 |
|
brcnvg |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ◡ 𝑅 𝑌 ↔ 𝑌 𝑅 𝑋 ) ) |
9 |
4 7 8
|
3bitrd |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) ) |