Step |
Hyp |
Ref |
Expression |
1 |
|
relcnv |
⊢ Rel ◡ ( 𝐴 ∘ ◡ 𝐵 ) |
2 |
|
relco |
⊢ Rel ( 𝐵 ∘ ◡ 𝐴 ) |
3 |
|
vex |
⊢ 𝑦 ∈ V |
4 |
|
vex |
⊢ 𝑧 ∈ V |
5 |
3 4
|
brcnv |
⊢ ( 𝑦 ◡ 𝐵 𝑧 ↔ 𝑧 𝐵 𝑦 ) |
6 |
|
vex |
⊢ 𝑥 ∈ V |
7 |
6 4
|
brcnv |
⊢ ( 𝑥 ◡ 𝐴 𝑧 ↔ 𝑧 𝐴 𝑥 ) |
8 |
7
|
bicomi |
⊢ ( 𝑧 𝐴 𝑥 ↔ 𝑥 ◡ 𝐴 𝑧 ) |
9 |
5 8
|
anbi12ci |
⊢ ( ( 𝑦 ◡ 𝐵 𝑧 ∧ 𝑧 𝐴 𝑥 ) ↔ ( 𝑥 ◡ 𝐴 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) |
10 |
9
|
exbii |
⊢ ( ∃ 𝑧 ( 𝑦 ◡ 𝐵 𝑧 ∧ 𝑧 𝐴 𝑥 ) ↔ ∃ 𝑧 ( 𝑥 ◡ 𝐴 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) |
11 |
6 3
|
opelcnv |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ ◡ ( 𝐴 ∘ ◡ 𝐵 ) ↔ 〈 𝑦 , 𝑥 〉 ∈ ( 𝐴 ∘ ◡ 𝐵 ) ) |
12 |
3 6
|
opelco |
⊢ ( 〈 𝑦 , 𝑥 〉 ∈ ( 𝐴 ∘ ◡ 𝐵 ) ↔ ∃ 𝑧 ( 𝑦 ◡ 𝐵 𝑧 ∧ 𝑧 𝐴 𝑥 ) ) |
13 |
11 12
|
bitri |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ ◡ ( 𝐴 ∘ ◡ 𝐵 ) ↔ ∃ 𝑧 ( 𝑦 ◡ 𝐵 𝑧 ∧ 𝑧 𝐴 𝑥 ) ) |
14 |
6 3
|
opelco |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ ( 𝐵 ∘ ◡ 𝐴 ) ↔ ∃ 𝑧 ( 𝑥 ◡ 𝐴 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) |
15 |
10 13 14
|
3bitr4i |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ ◡ ( 𝐴 ∘ ◡ 𝐵 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ( 𝐵 ∘ ◡ 𝐴 ) ) |
16 |
1 2 15
|
eqrelriiv |
⊢ ◡ ( 𝐴 ∘ ◡ 𝐵 ) = ( 𝐵 ∘ ◡ 𝐴 ) |