| Step | Hyp | Ref
| Expression |
| 1 | | trclexlem 15033 |
. 2
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V) |
| 2 | | ssun1 4178 |
. . 3
⊢ 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 3 | | relcnv 6122 |
. . . . . . . . . . . . . 14
⊢ Rel ◡𝑅 |
| 4 | | relssdmrn 6288 |
. . . . . . . . . . . . . 14
⊢ (Rel
◡𝑅 → ◡𝑅 ⊆ (dom ◡𝑅 × ran ◡𝑅)) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ◡𝑅 ⊆ (dom ◡𝑅 × ran ◡𝑅) |
| 6 | | ssequn1 4186 |
. . . . . . . . . . . . 13
⊢ (◡𝑅 ⊆ (dom ◡𝑅 × ran ◡𝑅) ↔ (◡𝑅 ∪ (dom ◡𝑅 × ran ◡𝑅)) = (dom ◡𝑅 × ran ◡𝑅)) |
| 7 | 5, 6 | mpbi 230 |
. . . . . . . . . . . 12
⊢ (◡𝑅 ∪ (dom ◡𝑅 × ran ◡𝑅)) = (dom ◡𝑅 × ran ◡𝑅) |
| 8 | | cnvun 6162 |
. . . . . . . . . . . . 13
⊢ ◡(𝑅 ∪ (dom 𝑅 × ran 𝑅)) = (◡𝑅 ∪ ◡(dom 𝑅 × ran 𝑅)) |
| 9 | | cnvxp 6177 |
. . . . . . . . . . . . . . 15
⊢ ◡(dom 𝑅 × ran 𝑅) = (ran 𝑅 × dom 𝑅) |
| 10 | | df-rn 5696 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝑅 = dom ◡𝑅 |
| 11 | | dfdm4 5906 |
. . . . . . . . . . . . . . . 16
⊢ dom 𝑅 = ran ◡𝑅 |
| 12 | 10, 11 | xpeq12i 5713 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑅 × dom 𝑅) = (dom ◡𝑅 × ran ◡𝑅) |
| 13 | 9, 12 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ ◡(dom 𝑅 × ran 𝑅) = (dom ◡𝑅 × ran ◡𝑅) |
| 14 | 13 | uneq2i 4165 |
. . . . . . . . . . . . 13
⊢ (◡𝑅 ∪ ◡(dom 𝑅 × ran 𝑅)) = (◡𝑅 ∪ (dom ◡𝑅 × ran ◡𝑅)) |
| 15 | 8, 14 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ◡(𝑅 ∪ (dom 𝑅 × ran 𝑅)) = (◡𝑅 ∪ (dom ◡𝑅 × ran ◡𝑅)) |
| 16 | 7, 15, 13 | 3eqtr4i 2775 |
. . . . . . . . . . 11
⊢ ◡(𝑅 ∪ (dom 𝑅 × ran 𝑅)) = ◡(dom 𝑅 × ran 𝑅) |
| 17 | 16 | breqi 5149 |
. . . . . . . . . 10
⊢ (𝑏◡(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑎 ↔ 𝑏◡(dom
𝑅 × ran 𝑅)𝑎) |
| 18 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
| 19 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
| 20 | 18, 19 | brcnv 5893 |
. . . . . . . . . 10
⊢ (𝑏◡(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑎 ↔ 𝑎(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏) |
| 21 | 18, 19 | brcnv 5893 |
. . . . . . . . . 10
⊢ (𝑏◡(dom 𝑅 × ran 𝑅)𝑎 ↔ 𝑎(dom 𝑅 × ran 𝑅)𝑏) |
| 22 | 17, 20, 21 | 3bitr3i 301 |
. . . . . . . . 9
⊢ (𝑎(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏 ↔ 𝑎(dom 𝑅 × ran 𝑅)𝑏) |
| 23 | 16 | breqi 5149 |
. . . . . . . . . 10
⊢ (𝑐◡(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏 ↔ 𝑐◡(dom
𝑅 × ran 𝑅)𝑏) |
| 24 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑐 ∈ V |
| 25 | 24, 18 | brcnv 5893 |
. . . . . . . . . 10
⊢ (𝑐◡(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏 ↔ 𝑏(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑐) |
| 26 | 24, 18 | brcnv 5893 |
. . . . . . . . . 10
⊢ (𝑐◡(dom 𝑅 × ran 𝑅)𝑏 ↔ 𝑏(dom 𝑅 × ran 𝑅)𝑐) |
| 27 | 23, 25, 26 | 3bitr3i 301 |
. . . . . . . . 9
⊢ (𝑏(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑐 ↔ 𝑏(dom 𝑅 × ran 𝑅)𝑐) |
| 28 | 22, 27 | anbi12i 628 |
. . . . . . . 8
⊢ ((𝑎(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏 ∧ 𝑏(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑐) ↔ (𝑎(dom 𝑅 × ran 𝑅)𝑏 ∧ 𝑏(dom 𝑅 × ran 𝑅)𝑐)) |
| 29 | 28 | biimpi 216 |
. . . . . . 7
⊢ ((𝑎(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏 ∧ 𝑏(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑐) → (𝑎(dom 𝑅 × ran 𝑅)𝑏 ∧ 𝑏(dom 𝑅 × ran 𝑅)𝑐)) |
| 30 | 29 | eximi 1835 |
. . . . . 6
⊢
(∃𝑏(𝑎(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏 ∧ 𝑏(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑐) → ∃𝑏(𝑎(dom 𝑅 × ran 𝑅)𝑏 ∧ 𝑏(dom 𝑅 × ran 𝑅)𝑐)) |
| 31 | 30 | ssopab2i 5555 |
. . . . 5
⊢
{〈𝑎, 𝑐〉 ∣ ∃𝑏(𝑎(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏 ∧ 𝑏(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑐)} ⊆ {〈𝑎, 𝑐〉 ∣ ∃𝑏(𝑎(dom 𝑅 × ran 𝑅)𝑏 ∧ 𝑏(dom 𝑅 × ran 𝑅)𝑐)} |
| 32 | | df-co 5694 |
. . . . 5
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = {〈𝑎, 𝑐〉 ∣ ∃𝑏(𝑎(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑏 ∧ 𝑏(𝑅 ∪ (dom 𝑅 × ran 𝑅))𝑐)} |
| 33 | | df-co 5694 |
. . . . 5
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) = {〈𝑎, 𝑐〉 ∣ ∃𝑏(𝑎(dom 𝑅 × ran 𝑅)𝑏 ∧ 𝑏(dom 𝑅 × ran 𝑅)𝑐)} |
| 34 | 31, 32, 33 | 3sstr4i 4035 |
. . . 4
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
| 35 | | xptrrel 15019 |
. . . . 5
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (dom 𝑅 × ran 𝑅) |
| 36 | | ssun2 4179 |
. . . . 5
⊢ (dom
𝑅 × ran 𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 37 | 35, 36 | sstri 3993 |
. . . 4
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 38 | 34, 37 | sstri 3993 |
. . 3
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 39 | | trcleq2lem 15030 |
. . . . 5
⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → ((𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥) ↔ (𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∧ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))))) |
| 40 | 39 | elabg 3676 |
. . . 4
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ↔ (𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∧ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))))) |
| 41 | 40 | biimprd 248 |
. . 3
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V → ((𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∧ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)})) |
| 42 | 2, 38, 41 | mp2ani 698 |
. 2
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)}) |
| 43 | 1, 42 | syl 17 |
1
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)}) |