Proof of Theorem trclubgNEW
| Step | Hyp | Ref
| Expression |
| 1 | | trclubgNEW.rex |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
| 2 | 1 | dmexd 7925 |
. . . 4
⊢ (𝜑 → dom 𝑅 ∈ V) |
| 3 | | rnexg 7924 |
. . . . 5
⊢ (𝑅 ∈ V → ran 𝑅 ∈ V) |
| 4 | 1, 3 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑅 ∈ V) |
| 5 | 2, 4 | xpexd 7771 |
. . 3
⊢ (𝜑 → (dom 𝑅 × ran 𝑅) ∈ V) |
| 6 | 1, 5 | unexd 7774 |
. 2
⊢ (𝜑 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V) |
| 7 | | id 22 |
. . . 4
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → 𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 8 | 7, 7 | coeq12d 5875 |
. . 3
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → (𝑥 ∘ 𝑥) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 9 | 8, 7 | sseq12d 4017 |
. 2
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → ((𝑥 ∘ 𝑥) ⊆ 𝑥 ↔ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 10 | | ssun1 4178 |
. . 3
⊢ 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 11 | 10 | a1i 11 |
. 2
⊢ (𝜑 → 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 12 | | cnvssrndm 6291 |
. . 3
⊢ ◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) |
| 13 | | coundi 6267 |
. . . 4
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
| 14 | | cnvss 5883 |
. . . . . . . 8
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅)) |
| 15 | | coss2 5867 |
. . . . . . . 8
⊢ (◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅))) |
| 16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅))) |
| 17 | | cocnvcnv2 6278 |
. . . . . . 7
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) |
| 18 | | cnvxp 6177 |
. . . . . . . 8
⊢ ◡(ran 𝑅 × dom 𝑅) = (dom 𝑅 × ran 𝑅) |
| 19 | 18 | coeq2i 5871 |
. . . . . . 7
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅)) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) |
| 20 | 16, 17, 19 | 3sstr3g 4036 |
. . . . . 6
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
| 21 | | ssequn1 4186 |
. . . . . 6
⊢ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ↔ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
| 22 | 20, 21 | sylib 218 |
. . . . 5
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
| 23 | | coundir 6268 |
. . . . . 6
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) = ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 24 | | coss1 5866 |
. . . . . . . . . 10
⊢ (◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅) → (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 25 | 14, 24 | syl 17 |
. . . . . . . . 9
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 26 | | cocnvcnv1 6277 |
. . . . . . . . 9
⊢ (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) = (𝑅 ∘ (dom 𝑅 × ran 𝑅)) |
| 27 | 18 | coeq1i 5870 |
. . . . . . . . 9
⊢ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅)) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
| 28 | 25, 26, 27 | 3sstr3g 4036 |
. . . . . . . 8
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 29 | | ssequn1 4186 |
. . . . . . . 8
⊢ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ↔ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 30 | 28, 29 | sylib 218 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 31 | | xptrrel 15019 |
. . . . . . . . 9
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (dom 𝑅 × ran 𝑅) |
| 32 | | ssun2 4179 |
. . . . . . . . 9
⊢ (dom
𝑅 × ran 𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 33 | 31, 32 | sstri 3993 |
. . . . . . . 8
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 34 | 33 | a1i 11 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 35 | 30, 34 | eqsstrd 4018 |
. . . . . 6
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 36 | 23, 35 | eqsstrid 4022 |
. . . . 5
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 37 | 22, 36 | eqsstrd 4018 |
. . . 4
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 38 | 13, 37 | eqsstrid 4022 |
. . 3
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 39 | 12, 38 | mp1i 13 |
. 2
⊢ (𝜑 → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 40 | 6, 9, 11, 39 | clublem 43623 |
1
⊢ (𝜑 → ∩ {𝑥
∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |