Proof of Theorem cover2
Step | Hyp | Ref
| Expression |
1 | | cover2.1 |
. . . 4
⊢ 𝐵 ∈ V |
2 | | ssrab2 3993 |
. . . 4
⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐵 |
3 | 1, 2 | elpwi2 5239 |
. . 3
⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} ∈ 𝒫 𝐵 |
4 | | nfra1 3140 |
. . . . 5
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) |
5 | 2 | unissi 4828 |
. . . . . . . 8
⊢ ∪ {𝑦
∈ 𝐵 ∣ 𝜑} ⊆ ∪ 𝐵 |
6 | 5 | sseli 3896 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ {𝑦
∈ 𝐵 ∣ 𝜑} → 𝑥 ∈ ∪ 𝐵) |
7 | | cover2.2 |
. . . . . . 7
⊢ 𝐴 = ∪
𝐵 |
8 | 6, 7 | eleqtrrdi 2849 |
. . . . . 6
⊢ (𝑥 ∈ ∪ {𝑦
∈ 𝐵 ∣ 𝜑} → 𝑥 ∈ 𝐴) |
9 | | rsp 3127 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))) |
10 | | elunirab 4835 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ {𝑦
∈ 𝐵 ∣ 𝜑} ↔ ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)) |
11 | 9, 10 | syl6ibr 255 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑})) |
12 | 8, 11 | impbid2 229 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴)) |
13 | 4, 12 | alrimi 2211 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴)) |
14 | | dfcleq 2730 |
. . . 4
⊢ (∪ {𝑦
∈ 𝐵 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴)) |
15 | 13, 14 | sylibr 237 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴) |
16 | | nfrab1 3296 |
. . . . . . 7
⊢
Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝜑} |
17 | 16 | nfeq2 2921 |
. . . . . 6
⊢
Ⅎ𝑦 𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} |
18 | | eleq2 2826 |
. . . . . . 7
⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑})) |
19 | | rabid 3290 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ 𝜑)) |
20 | 19 | simprbi 500 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝜑) |
21 | 18, 20 | syl6bi 256 |
. . . . . 6
⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (𝑦 ∈ 𝑧 → 𝜑)) |
22 | 17, 21 | ralrimi 3137 |
. . . . 5
⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ∀𝑦 ∈ 𝑧 𝜑) |
23 | | unieq 4830 |
. . . . . . 7
⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ∪ 𝑧 = ∪
{𝑦 ∈ 𝐵 ∣ 𝜑}) |
24 | 23 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (∪ 𝑧 = 𝐴 ↔ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴)) |
25 | 24 | anbi1d 633 |
. . . . 5
⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ((∪
𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) ↔ (∪
{𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))) |
26 | 22, 25 | mpbiran2d 708 |
. . . 4
⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ((∪
𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) ↔ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴)) |
27 | 26 | rspcev 3537 |
. . 3
⊢ (({𝑦 ∈ 𝐵 ∣ 𝜑} ∈ 𝒫 𝐵 ∧ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴) → ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) |
28 | 3, 15, 27 | sylancr 590 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) |
29 | | elpwi 4522 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 𝐵 → 𝑧 ⊆ 𝐵) |
30 | | r19.29r 3177 |
. . . . . . . . . . 11
⊢
((∃𝑦 ∈
𝑧 𝑥 ∈ 𝑦 ∧ ∀𝑦 ∈ 𝑧 𝜑) → ∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑)) |
31 | 30 | expcom 417 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑧 𝜑 → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑))) |
32 | | ssrexv 3968 |
. . . . . . . . . 10
⊢ (𝑧 ⊆ 𝐵 → (∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))) |
33 | 31, 32 | sylan9r 512 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))) |
34 | 29, 33 | sylan 583 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))) |
35 | | eleq2 2826 |
. . . . . . . . . 10
⊢ (∪ 𝑧 =
𝐴 → (𝑥 ∈ ∪ 𝑧
↔ 𝑥 ∈ 𝐴)) |
36 | 35 | biimpar 481 |
. . . . . . . . 9
⊢ ((∪ 𝑧 =
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪ 𝑧) |
37 | | eluni2 4823 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑧
↔ ∃𝑦 ∈
𝑧 𝑥 ∈ 𝑦) |
38 | 36, 37 | sylib 221 |
. . . . . . . 8
⊢ ((∪ 𝑧 =
𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦) |
39 | 34, 38 | impel 509 |
. . . . . . 7
⊢ (((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ (∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)) |
40 | 39 | anassrs 471 |
. . . . . 6
⊢ ((((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ ∪ 𝑧 = 𝐴) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)) |
41 | 40 | ralrimiva 3105 |
. . . . 5
⊢ (((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ ∪ 𝑧 = 𝐴) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)) |
42 | 41 | anasss 470 |
. . . 4
⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ (∀𝑦 ∈ 𝑧 𝜑 ∧ ∪ 𝑧 = 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)) |
43 | 42 | ancom2s 650 |
. . 3
⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ (∪ 𝑧 =
𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)) |
44 | 43 | rexlimiva 3200 |
. 2
⊢
(∃𝑧 ∈
𝒫 𝐵(∪ 𝑧 =
𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)) |
45 | 28, 44 | impbii 212 |
1
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) |