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⟩𝐹𝐶)) |
