Proof of Theorem xpiderm
Step | Hyp | Ref
| Expression |
1 | | relxp 4447 |
. . 3
⊢ Rel
(𝐴 × 𝐴) |
2 | 1 | a1i 9 |
. 2
⊢
(∃𝑥 𝑥 ∈ 𝐴 → Rel (𝐴 × 𝐴)) |
3 | | dmxpm 4555 |
. 2
⊢
(∃𝑥 𝑥 ∈ 𝐴 → dom (𝐴 × 𝐴) = 𝐴) |
4 | | cnvxp 4742 |
. . . 4
⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴) |
5 | | xpidtr 4715 |
. . . 4
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) |
6 | | uneq1 3090 |
. . . . 5
⊢ (◡(𝐴 × 𝐴) = (𝐴 × 𝐴) → (◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∪ (𝐴 × 𝐴))) |
7 | | unss2 3114 |
. . . . 5
⊢ (((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴))) |
8 | | unidm 3086 |
. . . . . 6
⊢ ((𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = (𝐴 × 𝐴) |
9 | | eqtr 2057 |
. . . . . . 7
⊢ (((◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) ∧ ((𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) → (◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) |
10 | | sseq2 2967 |
. . . . . . . 8
⊢ ((◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = (𝐴 × 𝐴) → ((◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) ↔ (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))) |
11 | 10 | biimpd 132 |
. . . . . . 7
⊢ ((◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = (𝐴 × 𝐴) → ((◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) → (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))) |
12 | 9, 11 | syl 14 |
. . . . . 6
⊢ (((◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) ∧ ((𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) → ((◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) → (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))) |
13 | 8, 12 | mpan2 401 |
. . . . 5
⊢ ((◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) → ((◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (◡(𝐴 × 𝐴) ∪ (𝐴 × 𝐴)) → (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))) |
14 | 6, 7, 13 | syl2im 34 |
. . . 4
⊢ (◡(𝐴 × 𝐴) = (𝐴 × 𝐴) → (((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))) |
15 | 4, 5, 14 | mp2 16 |
. . 3
⊢ (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴) |
16 | 15 | a1i 9 |
. 2
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴)) |
17 | | df-er 6106 |
. 2
⊢ ((𝐴 × 𝐴) Er 𝐴 ↔ (Rel (𝐴 × 𝐴) ∧ dom (𝐴 × 𝐴) = 𝐴 ∧ (◡(𝐴 × 𝐴) ∪ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))) |
18 | 2, 3, 16, 17 | syl3anbrc 1088 |
1
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (𝐴 × 𝐴) Er 𝐴) |