Proof of Theorem brtpos
Step | Hyp | Ref
| Expression |
1 | | brtpos2 7881 |
. . . . 5
⊢ (𝐶 ∈ 𝑉 → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
2 | 1 | adantr 484 |
. . . 4
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
3 | | opex 5321 |
. . . . . . . . . 10
⊢
〈𝐵, 𝐴〉 ∈ V |
4 | | breldmg 5742 |
. . . . . . . . . . 11
⊢
((〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑉 ∧ 〈𝐵, 𝐴〉𝐹𝐶) → 〈𝐵, 𝐴〉 ∈ dom 𝐹) |
5 | 4 | 3expia 1118 |
. . . . . . . . . 10
⊢
((〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑉) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
6 | 3, 5 | mpan 689 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
7 | 6 | adantr 484 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
8 | | opelcnvg 5715 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 ↔ 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
9 | 8 | adantl 485 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 ↔ 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
10 | 7, 9 | sylibrd 262 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐴, 𝐵〉 ∈ ◡dom 𝐹)) |
11 | | elun1 4103 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 → 〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅})) |
12 | 10, 11 | syl6 35 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}))) |
13 | 12 | pm4.71rd 566 |
. . . . 5
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 〈𝐵, 𝐴〉𝐹𝐶))) |
14 | | opswap 6053 |
. . . . . . 7
⊢ ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉 |
15 | 14 | breq1i 5037 |
. . . . . 6
⊢ (∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶) |
16 | 15 | anbi2i 625 |
. . . . 5
⊢
((〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶) ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 〈𝐵, 𝐴〉𝐹𝐶)) |
17 | 13, 16 | syl6bbr 292 |
. . . 4
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
18 | 2, 17 | bitr4d 285 |
. . 3
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |
19 | 18 | ex 416 |
. 2
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶))) |
20 | | brtpos0 7882 |
. . 3
⊢ (𝐶 ∈ 𝑉 → (∅tpos 𝐹𝐶 ↔ ∅𝐹𝐶)) |
21 | | opprc 4788 |
. . . . 5
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 = ∅) |
22 | 21 | breq1d 5040 |
. . . 4
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ ∅tpos 𝐹𝐶)) |
23 | | ancom 464 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐴 ∈ V)) |
24 | | opprc 4788 |
. . . . . 6
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → 〈𝐵, 𝐴〉 = ∅) |
25 | 24 | breq1d 5040 |
. . . . 5
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ ∅𝐹𝐶)) |
26 | 23, 25 | sylnbi 333 |
. . . 4
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ ∅𝐹𝐶)) |
27 | 22, 26 | bibi12d 349 |
. . 3
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → ((〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶) ↔ (∅tpos 𝐹𝐶 ↔ ∅𝐹𝐶))) |
28 | 20, 27 | syl5ibrcom 250 |
. 2
⊢ (𝐶 ∈ 𝑉 → (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶))) |
29 | 19, 28 | pm2.61d 182 |
1
⊢ (𝐶 ∈ 𝑉 → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |