| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → ∪ 𝑌 = 𝑋) |
| 2 | | dissnref.c |
. . . 4
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} |
| 3 | 2 | unisngl 23535 |
. . 3
⊢ 𝑋 = ∪
𝐶 |
| 4 | 1, 3 | eqtrdi 2793 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → ∪ 𝑌 = ∪
𝐶) |
| 5 | | simplr 769 |
. . . . . 6
⊢
((((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ (𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦)) → 𝑢 = {𝑥}) |
| 6 | | simprr 773 |
. . . . . . 7
⊢
((((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ (𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦)) → 𝑥 ∈ 𝑦) |
| 7 | 6 | snssd 4809 |
. . . . . 6
⊢
((((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ (𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦)) → {𝑥} ⊆ 𝑦) |
| 8 | 5, 7 | eqsstrd 4018 |
. . . . 5
⊢
((((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ (𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦)) → 𝑢 ⊆ 𝑦) |
| 9 | | simplr 769 |
. . . . . . 7
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑥 ∈ 𝑋) |
| 10 | | simp-4r 784 |
. . . . . . 7
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ∪ 𝑌 = 𝑋) |
| 11 | 9, 10 | eleqtrrd 2844 |
. . . . . 6
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑥 ∈ ∪ 𝑌) |
| 12 | | eluni2 4911 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝑌
↔ ∃𝑦 ∈
𝑌 𝑥 ∈ 𝑦) |
| 13 | 11, 12 | sylib 218 |
. . . . 5
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ∃𝑦 ∈ 𝑌 𝑥 ∈ 𝑦) |
| 14 | 8, 13 | reximddv 3171 |
. . . 4
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦) |
| 15 | 2 | eqabri 2885 |
. . . . . 6
⊢ (𝑢 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
| 16 | 15 | biimpi 216 |
. . . . 5
⊢ (𝑢 ∈ 𝐶 → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
| 17 | 16 | adantl 481 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) ∧ 𝑢 ∈ 𝐶) → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
| 18 | 14, 17 | r19.29a 3162 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) ∧ 𝑢 ∈ 𝐶) → ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦) |
| 19 | 18 | ralrimiva 3146 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → ∀𝑢 ∈ 𝐶 ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦) |
| 20 | | pwexg 5378 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V) |
| 21 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑥}) |
| 22 | | snelpwi 5448 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋) |
| 23 | 22 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → {𝑥} ∈ 𝒫 𝑋) |
| 24 | 21, 23 | eqeltrd 2841 |
. . . . . . . 8
⊢ (((𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝒫 𝑋) |
| 25 | 24, 16 | r19.29a 3162 |
. . . . . . 7
⊢ (𝑢 ∈ 𝐶 → 𝑢 ∈ 𝒫 𝑋) |
| 26 | 25 | ssriv 3987 |
. . . . . 6
⊢ 𝐶 ⊆ 𝒫 𝑋 |
| 27 | 26 | a1i 11 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝐶 ⊆ 𝒫 𝑋) |
| 28 | 20, 27 | ssexd 5324 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝐶 ∈ V) |
| 29 | 28 | adantr 480 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → 𝐶 ∈ V) |
| 30 | | eqid 2737 |
. . . 4
⊢ ∪ 𝐶 =
∪ 𝐶 |
| 31 | | eqid 2737 |
. . . 4
⊢ ∪ 𝑌 =
∪ 𝑌 |
| 32 | 30, 31 | isref 23517 |
. . 3
⊢ (𝐶 ∈ V → (𝐶Ref𝑌 ↔ (∪ 𝑌 = ∪
𝐶 ∧ ∀𝑢 ∈ 𝐶 ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦))) |
| 33 | 29, 32 | syl 17 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → (𝐶Ref𝑌 ↔ (∪ 𝑌 = ∪
𝐶 ∧ ∀𝑢 ∈ 𝐶 ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦))) |
| 34 | 4, 19, 33 | mpbir2and 713 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → 𝐶Ref𝑌) |