Proof of Theorem trclubgNEW
Step | Hyp | Ref
| Expression |
1 | | trclubgNEW.rex |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
2 | | dmexg 6989 |
. . . . 5
⊢ (𝑅 ∈ V → dom 𝑅 ∈ V) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝑅 ∈ V) |
4 | | rnexg 6990 |
. . . . 5
⊢ (𝑅 ∈ V → ran 𝑅 ∈ V) |
5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑅 ∈ V) |
6 | | xpexg 6858 |
. . . 4
⊢ ((dom
𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 × ran 𝑅) ∈ V) |
7 | 3, 5, 6 | syl2anc 691 |
. . 3
⊢ (𝜑 → (dom 𝑅 × ran 𝑅) ∈ V) |
8 | | unexg 6857 |
. . 3
⊢ ((𝑅 ∈ V ∧ (dom 𝑅 × ran 𝑅) ∈ V) → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V) |
9 | 1, 7, 8 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V) |
10 | | id 22 |
. . . 4
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → 𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
11 | 10, 10 | coeq12d 5208 |
. . 3
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → (𝑥 ∘ 𝑥) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
12 | 11, 10 | sseq12d 3597 |
. 2
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → ((𝑥 ∘ 𝑥) ⊆ 𝑥 ↔ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
13 | | ssun1 3738 |
. . 3
⊢ 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
14 | 13 | a1i 11 |
. 2
⊢ (𝜑 → 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
15 | | cnvssrndm 5574 |
. . 3
⊢ ◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) |
16 | | coundi 5553 |
. . . 4
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
17 | | cnvss 5216 |
. . . . . . . 8
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅)) |
18 | | coss2 5200 |
. . . . . . . 8
⊢ (◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅))) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅))) |
20 | | cocnvcnv2 5564 |
. . . . . . 7
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) |
21 | | cnvxp 5470 |
. . . . . . . 8
⊢ ◡(ran 𝑅 × dom 𝑅) = (dom 𝑅 × ran 𝑅) |
22 | 21 | coeq2i 5204 |
. . . . . . 7
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅)) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) |
23 | 19, 20, 22 | 3sstr3g 3608 |
. . . . . 6
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
24 | | ssequn1 3745 |
. . . . . 6
⊢ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ↔ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
25 | 23, 24 | sylib 207 |
. . . . 5
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
26 | | coundir 5554 |
. . . . . 6
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) = ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
27 | | coss1 5199 |
. . . . . . . . . 10
⊢ (◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅) → (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
28 | 17, 27 | syl 17 |
. . . . . . . . 9
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
29 | | cocnvcnv1 5563 |
. . . . . . . . 9
⊢ (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) = (𝑅 ∘ (dom 𝑅 × ran 𝑅)) |
30 | 21 | coeq1i 5203 |
. . . . . . . . 9
⊢ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅)) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
31 | 28, 29, 30 | 3sstr3g 3608 |
. . . . . . . 8
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
32 | | ssequn1 3745 |
. . . . . . . 8
⊢ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ↔ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
33 | 31, 32 | sylib 207 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
34 | | xptrrel 13567 |
. . . . . . . . 9
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (dom 𝑅 × ran 𝑅) |
35 | | ssun2 3739 |
. . . . . . . . 9
⊢ (dom
𝑅 × ran 𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
36 | 34, 35 | sstri 3577 |
. . . . . . . 8
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
37 | 36 | a1i 11 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
38 | 33, 37 | eqsstrd 3602 |
. . . . . 6
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
39 | 26, 38 | syl5eqss 3612 |
. . . . 5
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
40 | 25, 39 | eqsstrd 3602 |
. . . 4
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
41 | 16, 40 | syl5eqss 3612 |
. . 3
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
42 | 15, 41 | mp1i 13 |
. 2
⊢ (𝜑 → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
43 | 9, 12, 14, 42 | clublem 36936 |
1
⊢ (𝜑 → ∩ {𝑥
∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |