Proof of Theorem brtposg
Step | Hyp | Ref
| Expression |
1 | | opswapg 5072 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉) |
2 | 1 | breq1d 3975 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |
3 | 2 | 3adant3 1002 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |
4 | 3 | anbi2d 460 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶) ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 〈𝐵, 𝐴〉𝐹𝐶))) |
5 | | brtpos2 6198 |
. . 3
⊢ (𝐶 ∈ 𝑋 → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
6 | 5 | 3ad2ant3 1005 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
7 | | opexg 4188 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 〈𝐵, 𝐴〉 ∈ V) |
8 | 7 | ancoms 266 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐵, 𝐴〉 ∈ V) |
9 | 8 | anim1i 338 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑋)) |
10 | 9 | 3impa 1177 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑋)) |
11 | | breldmg 4792 |
. . . . . . 7
⊢
((〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑋 ∧ 〈𝐵, 𝐴〉𝐹𝐶) → 〈𝐵, 𝐴〉 ∈ dom 𝐹) |
12 | 11 | 3expia 1187 |
. . . . . 6
⊢
((〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
13 | 10, 12 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
14 | | opelcnvg 4766 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 ↔ 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
15 | 14 | 3adant3 1002 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 ↔ 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
16 | 13, 15 | sylibrd 168 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐴, 𝐵〉 ∈ ◡dom 𝐹)) |
17 | | elun1 3274 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 → 〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅})) |
18 | 16, 17 | syl6 33 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}))) |
19 | 18 | pm4.71rd 392 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 〈𝐵, 𝐴〉𝐹𝐶))) |
20 | 4, 6, 19 | 3bitr4d 219 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |