Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → ∪ 𝑌 = 𝑋) |
2 | | dissnref.c |
. . . 4
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} |
3 | 2 | unisngl 21140 |
. . 3
⊢ 𝑋 = ∪
𝐶 |
4 | 1, 3 | syl6eq 2660 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → ∪ 𝑌 = ∪
𝐶) |
5 | | simplr 788 |
. . . . . 6
⊢
((((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ (𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦)) → 𝑢 = {𝑥}) |
6 | | simprr 792 |
. . . . . . 7
⊢
((((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ (𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦)) → 𝑥 ∈ 𝑦) |
7 | 6 | snssd 4281 |
. . . . . 6
⊢
((((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ (𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦)) → {𝑥} ⊆ 𝑦) |
8 | 5, 7 | eqsstrd 3602 |
. . . . 5
⊢
((((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ (𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑦)) → 𝑢 ⊆ 𝑦) |
9 | | simplr 788 |
. . . . . . 7
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑥 ∈ 𝑋) |
10 | | simp-4r 803 |
. . . . . . 7
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ∪ 𝑌 = 𝑋) |
11 | 9, 10 | eleqtrrd 2691 |
. . . . . 6
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑥 ∈ ∪ 𝑌) |
12 | | eluni2 4376 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝑌
↔ ∃𝑦 ∈
𝑌 𝑥 ∈ 𝑦) |
13 | 11, 12 | sylib 207 |
. . . . 5
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ∃𝑦 ∈ 𝑌 𝑥 ∈ 𝑦) |
14 | 8, 13 | reximddv 3001 |
. . . 4
⊢
(((((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 =
𝑋) ∧ 𝑢 ∈ 𝐶) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦) |
15 | 2 | abeq2i 2722 |
. . . . . 6
⊢ (𝑢 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
16 | 15 | biimpi 205 |
. . . . 5
⊢ (𝑢 ∈ 𝐶 → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
17 | 16 | adantl 481 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) ∧ 𝑢 ∈ 𝐶) → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
18 | 14, 17 | r19.29a 3060 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) ∧ 𝑢 ∈ 𝐶) → ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦) |
19 | 18 | ralrimiva 2949 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → ∀𝑢 ∈ 𝐶 ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦) |
20 | | pwexg 4776 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V) |
21 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑥}) |
22 | | snelpwi 4839 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋) |
23 | 22 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → {𝑥} ∈ 𝒫 𝑋) |
24 | 21, 23 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝑢 ∈ 𝐶 ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝒫 𝑋) |
25 | 24, 16 | r19.29a 3060 |
. . . . . . 7
⊢ (𝑢 ∈ 𝐶 → 𝑢 ∈ 𝒫 𝑋) |
26 | 25 | ssriv 3572 |
. . . . . 6
⊢ 𝐶 ⊆ 𝒫 𝑋 |
27 | 26 | a1i 11 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝐶 ⊆ 𝒫 𝑋) |
28 | 20, 27 | ssexd 4733 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝐶 ∈ V) |
29 | 28 | adantr 480 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → 𝐶 ∈ V) |
30 | | eqid 2610 |
. . . 4
⊢ ∪ 𝐶 =
∪ 𝐶 |
31 | | eqid 2610 |
. . . 4
⊢ ∪ 𝑌 =
∪ 𝑌 |
32 | 30, 31 | isref 21122 |
. . 3
⊢ (𝐶 ∈ V → (𝐶Ref𝑌 ↔ (∪ 𝑌 = ∪
𝐶 ∧ ∀𝑢 ∈ 𝐶 ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦))) |
33 | 29, 32 | syl 17 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → (𝐶Ref𝑌 ↔ (∪ 𝑌 = ∪
𝐶 ∧ ∀𝑢 ∈ 𝐶 ∃𝑦 ∈ 𝑌 𝑢 ⊆ 𝑦))) |
34 | 4, 19, 33 | mpbir2and 959 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → 𝐶Ref𝑌) |