| Step | Hyp | Ref
| Expression |
| 1 | | ss2iundf.xph |
. . 3
⊢
Ⅎ𝑥𝜑 |
| 2 | | ss2iundf.ss |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) |
| 3 | | df-ral 3062 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐶 ¬ 𝐵 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷)) |
| 4 | | ss2iundf.el |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) |
| 5 | | ss2iundf.yph |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝜑 |
| 6 | | ss2iundf.a |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝐴 |
| 7 | 6 | nfcri 2897 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑥 ∈ 𝐴 |
| 8 | 5, 7 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ 𝐴) |
| 9 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌) |
| 10 | 9 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = 𝑌) → (𝑦 ∈ 𝐶 ↔ 𝑌 ∈ 𝐶)) |
| 11 | 10 | biimprd 248 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = 𝑌) → (𝑌 ∈ 𝐶 → 𝑦 ∈ 𝐶)) |
| 12 | | ss2iundf.sub |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) |
| 13 | 12 | sseq2d 4016 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → (𝐵 ⊆ 𝐷 ↔ 𝐵 ⊆ 𝐺)) |
| 14 | 13 | 3expa 1119 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = 𝑌) → (𝐵 ⊆ 𝐷 ↔ 𝐵 ⊆ 𝐺)) |
| 15 | 14 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = 𝑌) → (¬ 𝐵 ⊆ 𝐷 ↔ ¬ 𝐵 ⊆ 𝐺)) |
| 16 | 15 | biimpd 229 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = 𝑌) → (¬ 𝐵 ⊆ 𝐷 → ¬ 𝐵 ⊆ 𝐺)) |
| 17 | 11, 16 | imim12d 81 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = 𝑌) → ((𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷) → (𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺))) |
| 18 | 17 | ex 412 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝑌 → ((𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷) → (𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺)))) |
| 19 | 8, 18 | alrimi 2213 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 = 𝑌 → ((𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷) → (𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺)))) |
| 20 | | ss2iundf.y |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝑌 |
| 21 | | ss2iundf.yc |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝐶 |
| 22 | 20, 21 | nfel 2920 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑌 ∈ 𝐶 |
| 23 | | ss2iundf.b |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝐵 |
| 24 | | ss2iundf.g |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝐺 |
| 25 | 23, 24 | nfss 3976 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝐵 ⊆ 𝐺 |
| 26 | 25 | nfn 1857 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 ¬ 𝐵 ⊆ 𝐺 |
| 27 | 22, 26 | nfim 1896 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺) |
| 28 | 27, 20 | spcimgfi1 3547 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦 = 𝑌 → ((𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷) → (𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺))) → (𝑌 ∈ 𝐶 → (∀𝑦(𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷) → (𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺)))) |
| 29 | 19, 4, 28 | sylc 65 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦(𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷) → (𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺))) |
| 30 | 4, 29 | mpid 44 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦(𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷) → ¬ 𝐵 ⊆ 𝐺)) |
| 31 | 3, 30 | biimtrid 242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷 → ¬ 𝐵 ⊆ 𝐺)) |
| 32 | 31 | con2d 134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ⊆ 𝐺 → ¬ ∀𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷)) |
| 33 | | dfrex2 3073 |
. . . . 5
⊢
(∃𝑦 ∈
𝐶 𝐵 ⊆ 𝐷 ↔ ¬ ∀𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷) |
| 34 | 32, 33 | imbitrrdi 252 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ⊆ 𝐺 → ∃𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷)) |
| 35 | 2, 34 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷) |
| 36 | 1, 35 | ralrimia 3258 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷) |
| 37 | | ssel 3977 |
. . . . . . . 8
⊢ (𝐵 ⊆ 𝐷 → (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷)) |
| 38 | 37 | reximi 3084 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 𝐵 ⊆ 𝐷 → ∃𝑦 ∈ 𝐶 (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷)) |
| 39 | 23 | nfcri 2897 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑧 ∈ 𝐵 |
| 40 | 39 | r19.37 3262 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷) → (𝑧 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑧 ∈ 𝐷)) |
| 41 | 38, 40 | syl 17 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐶 𝐵 ⊆ 𝐷 → (𝑧 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑧 ∈ 𝐷)) |
| 42 | | eliun 4995 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ ∃𝑦 ∈ 𝐶 𝑧 ∈ 𝐷) |
| 43 | 41, 42 | imbitrrdi 252 |
. . . . 5
⊢
(∃𝑦 ∈
𝐶 𝐵 ⊆ 𝐷 → (𝑧 ∈ 𝐵 → 𝑧 ∈ ∪
𝑦 ∈ 𝐶 𝐷)) |
| 44 | 43 | ssrdv 3989 |
. . . 4
⊢
(∃𝑦 ∈
𝐶 𝐵 ⊆ 𝐷 → 𝐵 ⊆ ∪
𝑦 ∈ 𝐶 𝐷) |
| 45 | 44 | ralimi 3083 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪
𝑦 ∈ 𝐶 𝐷) |
| 46 | | ss2iundf.xc |
. . . . 5
⊢
Ⅎ𝑥𝐶 |
| 47 | | ss2iundf.d |
. . . . 5
⊢
Ⅎ𝑥𝐷 |
| 48 | 46, 47 | nfiun 5023 |
. . . 4
⊢
Ⅎ𝑥∪ 𝑦 ∈ 𝐶 𝐷 |
| 49 | 48 | iunssf 5044 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪
𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ∪
𝑦 ∈ 𝐶 𝐷) |
| 50 | 45, 49 | sylibr 234 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ∪
𝑥 ∈ 𝐴 𝐵 ⊆ ∪
𝑦 ∈ 𝐶 𝐷) |
| 51 | 36, 50 | syl 17 |
1
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪
𝑦 ∈ 𝐶 𝐷) |