Proof of Theorem brtpos
| Step | Hyp | Ref
| Expression |
| 1 | | brtpos2 8257 |
. . . . 5
⊢ (𝐶 ∈ 𝑉 → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
| 3 | | opex 5469 |
. . . . . . . . . 10
⊢
〈𝐵, 𝐴〉 ∈ V |
| 4 | | breldmg 5920 |
. . . . . . . . . . 11
⊢
((〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑉 ∧ 〈𝐵, 𝐴〉𝐹𝐶) → 〈𝐵, 𝐴〉 ∈ dom 𝐹) |
| 5 | 4 | 3expia 1122 |
. . . . . . . . . 10
⊢
((〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑉) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
| 6 | 3, 5 | mpan 690 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
| 8 | | opelcnvg 5891 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 ↔ 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
| 9 | 8 | adantl 481 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 ↔ 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
| 10 | 7, 9 | sylibrd 259 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐴, 𝐵〉 ∈ ◡dom 𝐹)) |
| 11 | | elun1 4182 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 → 〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅})) |
| 12 | 10, 11 | syl6 35 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}))) |
| 13 | 12 | pm4.71rd 562 |
. . . . 5
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 〈𝐵, 𝐴〉𝐹𝐶))) |
| 14 | | opswap 6249 |
. . . . . . 7
⊢ ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉 |
| 15 | 14 | breq1i 5150 |
. . . . . 6
⊢ (∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶) |
| 16 | 15 | anbi2i 623 |
. . . . 5
⊢
((〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶) ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 〈𝐵, 𝐴〉𝐹𝐶)) |
| 17 | 13, 16 | bitr4di 289 |
. . . 4
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
| 18 | 2, 17 | bitr4d 282 |
. . 3
⊢ ((𝐶 ∈ 𝑉 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |
| 19 | 18 | ex 412 |
. 2
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶))) |
| 20 | | brtpos0 8258 |
. . 3
⊢ (𝐶 ∈ 𝑉 → (∅tpos 𝐹𝐶 ↔ ∅𝐹𝐶)) |
| 21 | | opprc 4896 |
. . . . 5
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 = ∅) |
| 22 | 21 | breq1d 5153 |
. . . 4
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ ∅tpos 𝐹𝐶)) |
| 23 | | ancom 460 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐴 ∈ V)) |
| 24 | | opprc 4896 |
. . . . . 6
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → 〈𝐵, 𝐴〉 = ∅) |
| 25 | 24 | breq1d 5153 |
. . . . 5
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ ∅𝐹𝐶)) |
| 26 | 23, 25 | sylnbi 330 |
. . . 4
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ ∅𝐹𝐶)) |
| 27 | 22, 26 | bibi12d 345 |
. . 3
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → ((〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶) ↔ (∅tpos 𝐹𝐶 ↔ ∅𝐹𝐶))) |
| 28 | 20, 27 | syl5ibrcom 247 |
. 2
⊢ (𝐶 ∈ 𝑉 → (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶))) |
| 29 | 19, 28 | pm2.61d 179 |
1
⊢ (𝐶 ∈ 𝑉 → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |