Proof of Theorem brtposg
Step | Hyp | Ref
| Expression |
1 | | opswapg 4750 |
. . . . 5
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∪ ◡{〈A, B〉} =
〈B, A〉) |
2 | 1 | breq1d 3765 |
. . . 4
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → (∪ ◡{〈A, B〉}𝐹𝐶 ↔ 〈B, A〉𝐹𝐶)) |
3 | 2 | 3adant3 923 |
. . 3
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∪ ◡{〈A, B〉}𝐹𝐶 ↔ 〈B, A〉𝐹𝐶)) |
4 | 3 | anbi2d 437 |
. 2
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((〈A, B〉 ∈ (◡dom
𝐹 ∪ {∅}) ∧ ∪ ◡{〈A, B〉}𝐹𝐶) ↔ (〈A, B〉 ∈ (◡dom
𝐹 ∪ {∅}) ∧ 〈B,
A〉𝐹𝐶))) |
5 | | brtpos2 5807 |
. . 3
⊢ (𝐶 ∈ 𝑋 → (〈A, B〉tpos
𝐹𝐶 ↔ (〈A, B〉 ∈ (◡dom
𝐹 ∪ {∅}) ∧ ∪ ◡{〈A, B〉}𝐹𝐶))) |
6 | 5 | 3ad2ant3 926 |
. 2
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈A, B〉tpos
𝐹𝐶 ↔ (〈A, B〉 ∈ (◡dom
𝐹 ∪ {∅}) ∧ ∪ ◡{〈A, B〉}𝐹𝐶))) |
7 | | opexg 3955 |
. . . . . . . . 9
⊢
((B ∈ 𝑊 ∧ A ∈ 𝑉) → 〈B, A〉 ∈ V) |
8 | 7 | ancoms 255 |
. . . . . . . 8
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → 〈B, A〉 ∈ V) |
9 | 8 | anim1i 323 |
. . . . . . 7
⊢
(((A ∈ 𝑉 ∧ B ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (〈B, A〉 ∈ V ∧ 𝐶 ∈ 𝑋)) |
10 | 9 | 3impa 1098 |
. . . . . 6
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈B, A〉 ∈ V ∧ 𝐶 ∈ 𝑋)) |
11 | | breldmg 4484 |
. . . . . . 7
⊢
((〈B, A〉 ∈ V ∧ 𝐶 ∈ 𝑋 ∧ 〈B,
A〉𝐹𝐶) → 〈B, A〉 ∈ dom 𝐹) |
12 | 11 | 3expia 1105 |
. . . . . 6
⊢
((〈B, A〉 ∈ V ∧ 𝐶 ∈ 𝑋) → (〈B, A〉𝐹𝐶 → 〈B, A〉 ∈ dom 𝐹)) |
13 | 10, 12 | syl 14 |
. . . . 5
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈B, A〉𝐹𝐶 → 〈B, A〉 ∈ dom 𝐹)) |
14 | | opelcnvg 4458 |
. . . . . 6
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → (〈A, B〉 ∈ ◡dom
𝐹 ↔ 〈B, A〉 ∈ dom 𝐹)) |
15 | 14 | 3adant3 923 |
. . . . 5
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈A, B〉 ∈ ◡dom
𝐹 ↔ 〈B, A〉 ∈ dom 𝐹)) |
16 | 13, 15 | sylibrd 158 |
. . . 4
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈B, A〉𝐹𝐶 → 〈A, B〉 ∈ ◡dom
𝐹)) |
17 | | elun1 3104 |
. . . 4
⊢
(〈A, B〉 ∈ ◡dom 𝐹 → 〈A, B〉 ∈ (◡dom
𝐹 ∪
{∅})) |
18 | 16, 17 | syl6 29 |
. . 3
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈B, A〉𝐹𝐶 → 〈A, B〉 ∈ (◡dom
𝐹 ∪
{∅}))) |
19 | 18 | pm4.71rd 374 |
. 2
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈B, A〉𝐹𝐶 ↔ (〈A, B〉 ∈ (◡dom
𝐹 ∪ {∅}) ∧ 〈B,
A〉𝐹𝐶))) |
20 | 4, 6, 19 | 3bitr4d 209 |
1
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈A, B〉tpos
𝐹𝐶 ↔ 〈B, A〉𝐹𝐶)) |