Proof of Theorem brtposg
Step | Hyp | Ref
| Expression |
1 | | opswapg 5115 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉) |
2 | 1 | breq1d 4013 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |
3 | 2 | 3adant3 1017 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |
4 | 3 | anbi2d 464 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶) ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 〈𝐵, 𝐴〉𝐹𝐶))) |
5 | | brtpos2 6251 |
. . 3
⊢ (𝐶 ∈ 𝑋 → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
6 | 5 | 3ad2ant3 1020 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{〈𝐴, 𝐵〉}𝐹𝐶))) |
7 | | opexg 4228 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 〈𝐵, 𝐴〉 ∈ V) |
8 | 7 | ancoms 268 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐵, 𝐴〉 ∈ V) |
9 | 8 | anim1i 340 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑋)) |
10 | 9 | 3impa 1194 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑋)) |
11 | | breldmg 4833 |
. . . . . . 7
⊢
((〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑋 ∧ 〈𝐵, 𝐴〉𝐹𝐶) → 〈𝐵, 𝐴〉 ∈ dom 𝐹) |
12 | 11 | 3expia 1205 |
. . . . . 6
⊢
((〈𝐵, 𝐴〉 ∈ V ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
13 | 10, 12 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
14 | | opelcnvg 4807 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 ↔ 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
15 | 14 | 3adant3 1017 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 ↔ 〈𝐵, 𝐴〉 ∈ dom 𝐹)) |
16 | 13, 15 | sylibrd 169 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐴, 𝐵〉 ∈ ◡dom 𝐹)) |
17 | | elun1 3302 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ∈ ◡dom 𝐹 → 〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅})) |
18 | 16, 17 | syl6 33 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 → 〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}))) |
19 | 18 | pm4.71rd 394 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐴〉𝐹𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (◡dom 𝐹 ∪ {∅}) ∧ 〈𝐵, 𝐴〉𝐹𝐶))) |
20 | 4, 6, 19 | 3bitr4d 220 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) |