Step |
Hyp |
Ref |
Expression |
1 |
|
brtpos2 |
⊢ ( 𝐶 ∈ 𝑉 → ( 〈 𝐴 , 𝐵 〉 tpos 𝐹 𝐶 ↔ ( 〈 𝐴 , 𝐵 〉 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 〈 𝐴 , 𝐵 〉 } 𝐹 𝐶 ) ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 〈 𝐴 , 𝐵 〉 tpos 𝐹 𝐶 ↔ ( 〈 𝐴 , 𝐵 〉 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 〈 𝐴 , 𝐵 〉 } 𝐹 𝐶 ) ) ) |
3 |
|
opex |
⊢ 〈 𝐵 , 𝐴 〉 ∈ V |
4 |
|
breldmg |
⊢ ( ( 〈 𝐵 , 𝐴 〉 ∈ V ∧ 𝐶 ∈ 𝑉 ∧ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) → 〈 𝐵 , 𝐴 〉 ∈ dom 𝐹 ) |
5 |
4
|
3expia |
⊢ ( ( 〈 𝐵 , 𝐴 〉 ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 → 〈 𝐵 , 𝐴 〉 ∈ dom 𝐹 ) ) |
6 |
3 5
|
mpan |
⊢ ( 𝐶 ∈ 𝑉 → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 → 〈 𝐵 , 𝐴 〉 ∈ dom 𝐹 ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 → 〈 𝐵 , 𝐴 〉 ∈ dom 𝐹 ) ) |
8 |
|
opelcnvg |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 〈 𝐴 , 𝐵 〉 ∈ ◡ dom 𝐹 ↔ 〈 𝐵 , 𝐴 〉 ∈ dom 𝐹 ) ) |
9 |
8
|
adantl |
⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 〈 𝐴 , 𝐵 〉 ∈ ◡ dom 𝐹 ↔ 〈 𝐵 , 𝐴 〉 ∈ dom 𝐹 ) ) |
10 |
7 9
|
sylibrd |
⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 → 〈 𝐴 , 𝐵 〉 ∈ ◡ dom 𝐹 ) ) |
11 |
|
elun1 |
⊢ ( 〈 𝐴 , 𝐵 〉 ∈ ◡ dom 𝐹 → 〈 𝐴 , 𝐵 〉 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) |
12 |
10 11
|
syl6 |
⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 → 〈 𝐴 , 𝐵 〉 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) ) |
13 |
12
|
pm4.71rd |
⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ↔ ( 〈 𝐴 , 𝐵 〉 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) ) ) |
14 |
|
opswap |
⊢ ∪ ◡ { 〈 𝐴 , 𝐵 〉 } = 〈 𝐵 , 𝐴 〉 |
15 |
14
|
breq1i |
⊢ ( ∪ ◡ { 〈 𝐴 , 𝐵 〉 } 𝐹 𝐶 ↔ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) |
16 |
15
|
anbi2i |
⊢ ( ( 〈 𝐴 , 𝐵 〉 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 〈 𝐴 , 𝐵 〉 } 𝐹 𝐶 ) ↔ ( 〈 𝐴 , 𝐵 〉 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) ) |
17 |
13 16
|
bitr4di |
⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ↔ ( 〈 𝐴 , 𝐵 〉 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 〈 𝐴 , 𝐵 〉 } 𝐹 𝐶 ) ) ) |
18 |
2 17
|
bitr4d |
⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 〈 𝐴 , 𝐵 〉 tpos 𝐹 𝐶 ↔ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) ) |
19 |
18
|
ex |
⊢ ( 𝐶 ∈ 𝑉 → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 〈 𝐴 , 𝐵 〉 tpos 𝐹 𝐶 ↔ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) ) ) |
20 |
|
brtpos0 |
⊢ ( 𝐶 ∈ 𝑉 → ( ∅ tpos 𝐹 𝐶 ↔ ∅ 𝐹 𝐶 ) ) |
21 |
|
opprc |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 〈 𝐴 , 𝐵 〉 = ∅ ) |
22 |
21
|
breq1d |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 〈 𝐴 , 𝐵 〉 tpos 𝐹 𝐶 ↔ ∅ tpos 𝐹 𝐶 ) ) |
23 |
|
ancom |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) |
24 |
|
opprc |
⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 〈 𝐵 , 𝐴 〉 = ∅ ) |
25 |
24
|
breq1d |
⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ↔ ∅ 𝐹 𝐶 ) ) |
26 |
23 25
|
sylnbi |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ↔ ∅ 𝐹 𝐶 ) ) |
27 |
22 26
|
bibi12d |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 〈 𝐴 , 𝐵 〉 tpos 𝐹 𝐶 ↔ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) ↔ ( ∅ tpos 𝐹 𝐶 ↔ ∅ 𝐹 𝐶 ) ) ) |
28 |
20 27
|
syl5ibrcom |
⊢ ( 𝐶 ∈ 𝑉 → ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 〈 𝐴 , 𝐵 〉 tpos 𝐹 𝐶 ↔ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) ) ) |
29 |
19 28
|
pm2.61d |
⊢ ( 𝐶 ∈ 𝑉 → ( 〈 𝐴 , 𝐵 〉 tpos 𝐹 𝐶 ↔ 〈 𝐵 , 𝐴 〉 𝐹 𝐶 ) ) |