Proof of Theorem trclubgNEW
Step | Hyp | Ref
| Expression |
1 | | trclubgNEW.rex |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
2 | | dmexg 7097 |
. . . . 5
⊢ (𝑅 ∈ V → dom 𝑅 ∈ V) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝑅 ∈ V) |
4 | | rnexg 7098 |
. . . . 5
⊢ (𝑅 ∈ V → ran 𝑅 ∈ V) |
5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑅 ∈ V) |
6 | | xpexg 6960 |
. . . 4
⊢ ((dom
𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 × ran 𝑅) ∈ V) |
7 | 3, 5, 6 | syl2anc 693 |
. . 3
⊢ (𝜑 → (dom 𝑅 × ran 𝑅) ∈ V) |
8 | | unexg 6959 |
. . 3
⊢ ((𝑅 ∈ V ∧ (dom 𝑅 × ran 𝑅) ∈ V) → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V) |
9 | 1, 7, 8 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V) |
10 | | id 22 |
. . . 4
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → 𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
11 | 10, 10 | coeq12d 5286 |
. . 3
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → (𝑥 ∘ 𝑥) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
12 | 11, 10 | sseq12d 3634 |
. 2
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → ((𝑥 ∘ 𝑥) ⊆ 𝑥 ↔ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
13 | | ssun1 3776 |
. . 3
⊢ 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
14 | 13 | a1i 11 |
. 2
⊢ (𝜑 → 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
15 | | cnvssrndm 5657 |
. . 3
⊢ ◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) |
16 | | coundi 5636 |
. . . 4
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
17 | | cnvss 5294 |
. . . . . . . 8
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅)) |
18 | | coss2 5278 |
. . . . . . . 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 5647 |
. . . . . . 7
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) |
21 | | cnvxp 5551 |
. . . . . . . 8
⊢ ◡(ran 𝑅 × dom 𝑅) = (dom 𝑅 × ran 𝑅) |
22 | 21 | coeq2i 5282 |
. . . . . . 7
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅)) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) |
23 | 19, 20, 22 | 3sstr3g 3645 |
. . . . . 6
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
24 | | ssequn1 3783 |
. . . . . 6
⊢ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ↔ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
25 | 23, 24 | sylib 208 |
. . . . 5
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
26 | | coundir 5637 |
. . . . . 6
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) = ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
27 | | coss1 5277 |
. . . . . . . . . 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 5646 |
. . . . . . . . 9
⊢ (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) = (𝑅 ∘ (dom 𝑅 × ran 𝑅)) |
30 | 21 | coeq1i 5281 |
. . . . . . . . 9
⊢ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅)) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
31 | 28, 29, 30 | 3sstr3g 3645 |
. . . . . . . 8
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
32 | | ssequn1 3783 |
. . . . . . . 8
⊢ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ↔ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
33 | 31, 32 | sylib 208 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
34 | | xptrrel 13719 |
. . . . . . . . 9
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (dom 𝑅 × ran 𝑅) |
35 | | ssun2 3777 |
. . . . . . . . 9
⊢ (dom
𝑅 × ran 𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
36 | 34, 35 | sstri 3612 |
. . . . . . . 8
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
37 | 36 | a1i 11 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
38 | 33, 37 | eqsstrd 3639 |
. . . . . 6
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
39 | 26, 38 | syl5eqss 3649 |
. . . . 5
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
40 | 25, 39 | eqsstrd 3639 |
. . . 4
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
41 | 16, 40 | syl5eqss 3649 |
. . 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 37917 |
1
⊢ (𝜑 → ∩ {𝑥
∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |