Proof of Theorem trclexi
| Step | Hyp | Ref
| Expression |
| 1 | | ssun1 4178 |
. 2
⊢ 𝐴 ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴)) |
| 2 | | coundir 6268 |
. . . 4
⊢ ((𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) = ((𝐴 ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ∪ ((dom 𝐴 × ran 𝐴) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴)))) |
| 3 | | coundi 6267 |
. . . . . 6
⊢ (𝐴 ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) = ((𝐴 ∘ 𝐴) ∪ (𝐴 ∘ (dom 𝐴 × ran 𝐴))) |
| 4 | | cossxp 6292 |
. . . . . . 7
⊢ (𝐴 ∘ 𝐴) ⊆ (dom 𝐴 × ran 𝐴) |
| 5 | | cossxp 6292 |
. . . . . . . 8
⊢ (𝐴 ∘ (dom 𝐴 × ran 𝐴)) ⊆ (dom (dom 𝐴 × ran 𝐴) × ran 𝐴) |
| 6 | | dmxpss 6191 |
. . . . . . . . 9
⊢ dom (dom
𝐴 × ran 𝐴) ⊆ dom 𝐴 |
| 7 | | xpss1 5704 |
. . . . . . . . 9
⊢ (dom (dom
𝐴 × ran 𝐴) ⊆ dom 𝐴 → (dom (dom 𝐴 × ran 𝐴) × ran 𝐴) ⊆ (dom 𝐴 × ran 𝐴)) |
| 8 | 6, 7 | ax-mp 5 |
. . . . . . . 8
⊢ (dom (dom
𝐴 × ran 𝐴) × ran 𝐴) ⊆ (dom 𝐴 × ran 𝐴) |
| 9 | 5, 8 | sstri 3993 |
. . . . . . 7
⊢ (𝐴 ∘ (dom 𝐴 × ran 𝐴)) ⊆ (dom 𝐴 × ran 𝐴) |
| 10 | 4, 9 | unssi 4191 |
. . . . . 6
⊢ ((𝐴 ∘ 𝐴) ∪ (𝐴 ∘ (dom 𝐴 × ran 𝐴))) ⊆ (dom 𝐴 × ran 𝐴) |
| 11 | 3, 10 | eqsstri 4030 |
. . . . 5
⊢ (𝐴 ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ⊆ (dom 𝐴 × ran 𝐴) |
| 12 | | coundi 6267 |
. . . . . 6
⊢ ((dom
𝐴 × ran 𝐴) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) = (((dom 𝐴 × ran 𝐴) ∘ 𝐴) ∪ ((dom 𝐴 × ran 𝐴) ∘ (dom 𝐴 × ran 𝐴))) |
| 13 | | cossxp 6292 |
. . . . . . . 8
⊢ ((dom
𝐴 × ran 𝐴) ∘ 𝐴) ⊆ (dom 𝐴 × ran (dom 𝐴 × ran 𝐴)) |
| 14 | | rnxpss 6192 |
. . . . . . . . 9
⊢ ran (dom
𝐴 × ran 𝐴) ⊆ ran 𝐴 |
| 15 | | xpss2 5705 |
. . . . . . . . 9
⊢ (ran (dom
𝐴 × ran 𝐴) ⊆ ran 𝐴 → (dom 𝐴 × ran (dom 𝐴 × ran 𝐴)) ⊆ (dom 𝐴 × ran 𝐴)) |
| 16 | 14, 15 | ax-mp 5 |
. . . . . . . 8
⊢ (dom
𝐴 × ran (dom 𝐴 × ran 𝐴)) ⊆ (dom 𝐴 × ran 𝐴) |
| 17 | 13, 16 | sstri 3993 |
. . . . . . 7
⊢ ((dom
𝐴 × ran 𝐴) ∘ 𝐴) ⊆ (dom 𝐴 × ran 𝐴) |
| 18 | | xptrrel 15019 |
. . . . . . 7
⊢ ((dom
𝐴 × ran 𝐴) ∘ (dom 𝐴 × ran 𝐴)) ⊆ (dom 𝐴 × ran 𝐴) |
| 19 | 17, 18 | unssi 4191 |
. . . . . 6
⊢ (((dom
𝐴 × ran 𝐴) ∘ 𝐴) ∪ ((dom 𝐴 × ran 𝐴) ∘ (dom 𝐴 × ran 𝐴))) ⊆ (dom 𝐴 × ran 𝐴) |
| 20 | 12, 19 | eqsstri 4030 |
. . . . 5
⊢ ((dom
𝐴 × ran 𝐴) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ⊆ (dom 𝐴 × ran 𝐴) |
| 21 | 11, 20 | unssi 4191 |
. . . 4
⊢ ((𝐴 ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ∪ ((dom 𝐴 × ran 𝐴) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴)))) ⊆ (dom 𝐴 × ran 𝐴) |
| 22 | 2, 21 | eqsstri 4030 |
. . 3
⊢ ((𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ⊆ (dom 𝐴 × ran 𝐴) |
| 23 | | ssun2 4179 |
. . 3
⊢ (dom
𝐴 × ran 𝐴) ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴)) |
| 24 | 22, 23 | sstri 3993 |
. 2
⊢ ((𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴)) |
| 25 | | trclexi.1 |
. . . . . 6
⊢ 𝐴 ∈ 𝑉 |
| 26 | 25 | elexi 3503 |
. . . . 5
⊢ 𝐴 ∈ V |
| 27 | 26 | dmex 7931 |
. . . . . 6
⊢ dom 𝐴 ∈ V |
| 28 | 26 | rnex 7932 |
. . . . . 6
⊢ ran 𝐴 ∈ V |
| 29 | 27, 28 | xpex 7773 |
. . . . 5
⊢ (dom
𝐴 × ran 𝐴) ∈ V |
| 30 | 26, 29 | unex 7764 |
. . . 4
⊢ (𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∈ V |
| 31 | | trcleq2lem 15030 |
. . . 4
⊢ (𝑥 = (𝐴 ∪ (dom 𝐴 × ran 𝐴)) → ((𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥) ↔ (𝐴 ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∧ ((𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴))))) |
| 32 | 30, 31 | spcev 3606 |
. . 3
⊢ ((𝐴 ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∧ ((𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)) |
| 33 | | intexab 5346 |
. . 3
⊢
(∃𝑥(𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥) ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V) |
| 34 | 32, 33 | sylib 218 |
. 2
⊢ ((𝐴 ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∧ ((𝐴 ∪ (dom 𝐴 × ran 𝐴)) ∘ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) ⊆ (𝐴 ∪ (dom 𝐴 × ran 𝐴))) → ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V) |
| 35 | 1, 24, 34 | mp2an 692 |
1
⊢ ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V |