Step | Hyp | Ref
| Expression |
1 | | trclubgNEW.rex |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
2 | 1 | dmexd 7900 |
. . . 4
⊢ (𝜑 → dom 𝑅 ∈ V) |
3 | | rnexg 7899 |
. . . . 5
⊢ (𝑅 ∈ V → ran 𝑅 ∈ V) |
4 | 1, 3 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑅 ∈ V) |
5 | 2, 4 | xpexd 7742 |
. . 3
⊢ (𝜑 → (dom 𝑅 × ran 𝑅) ∈ V) |
6 | 1, 5 | unexd 7745 |
. 2
⊢ (𝜑 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V) |
7 | | id 22 |
. . . 4
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → 𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
8 | 7, 7 | coeq12d 5864 |
. . 3
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → (𝑥 ∘ 𝑥) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
9 | 8, 7 | sseq12d 4015 |
. 2
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → ((𝑥 ∘ 𝑥) ⊆ 𝑥 ↔ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
10 | | ssun1 4172 |
. . 3
⊢ 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
11 | 10 | a1i 11 |
. 2
⊢ (𝜑 → 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
12 | | cnvssrndm 6270 |
. . 3
⊢ ◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) |
13 | | coundi 6246 |
. . . 4
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
14 | | cnvss 5872 |
. . . . . . . 8
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅)) |
15 | | coss2 5856 |
. . . . . . . 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 6257 |
. . . . . . 7
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) |
18 | | cnvxp 6156 |
. . . . . . . 8
⊢ ◡(ran 𝑅 × dom 𝑅) = (dom 𝑅 × ran 𝑅) |
19 | 18 | coeq2i 5860 |
. . . . . . 7
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅)) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) |
20 | 16, 17, 19 | 3sstr3g 4026 |
. . . . . 6
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
21 | | ssequn1 4180 |
. . . . . 6
⊢ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ↔ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
22 | 20, 21 | sylib 217 |
. . . . 5
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) |
23 | | coundir 6247 |
. . . . . 6
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) = ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
24 | | coss1 5855 |
. . . . . . . . . 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 6256 |
. . . . . . . . 9
⊢ (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) = (𝑅 ∘ (dom 𝑅 × ran 𝑅)) |
27 | 18 | coeq1i 5859 |
. . . . . . . . 9
⊢ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅)) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
28 | 25, 26, 27 | 3sstr3g 4026 |
. . . . . . . 8
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
29 | | ssequn1 4180 |
. . . . . . . 8
⊢ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ↔ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
30 | 28, 29 | sylib 217 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
31 | | xptrrel 14932 |
. . . . . . . . 9
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (dom 𝑅 × ran 𝑅) |
32 | | ssun2 4173 |
. . . . . . . . 9
⊢ (dom
𝑅 × ran 𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
33 | 31, 32 | sstri 3991 |
. . . . . . . 8
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
35 | 30, 34 | eqsstrd 4020 |
. . . . . 6
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
36 | 23, 35 | eqsstrid 4030 |
. . . . 5
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
37 | 22, 36 | eqsstrd 4020 |
. . . 4
⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
38 | 13, 37 | eqsstrid 4030 |
. . 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 42664 |
1
⊢ (𝜑 → ∩ {𝑥
∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |