Proof of Theorem eliuniin2
Step | Hyp | Ref
| Expression |
1 | | eliuniin2.2 |
. . . . . . 7
⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 |
2 | 1 | eleq2i 2680 |
. . . . . 6
⊢ (𝑍 ∈ 𝐴 ↔ 𝑍 ∈ ∪
𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷) |
3 | 2 | biimpi 205 |
. . . . 5
⊢ (𝑍 ∈ 𝐴 → 𝑍 ∈ ∪
𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷) |
4 | | eliun 4460 |
. . . . 5
⊢ (𝑍 ∈ ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
5 | 3, 4 | sylib 207 |
. . . 4
⊢ (𝑍 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
6 | | id 22 |
. . . . . . 7
⊢ (𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
7 | | eliin 4461 |
. . . . . . 7
⊢ (𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → (𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
8 | 6, 7 | mpbid 221 |
. . . . . 6
⊢ (𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) |
9 | 8 | a1i 11 |
. . . . 5
⊢ (𝑍 ∈ 𝐴 → (𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 → ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
10 | 9 | reximdv 2999 |
. . . 4
⊢ (𝑍 ∈ 𝐴 → (∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
11 | 5, 10 | mpd 15 |
. . 3
⊢ (𝑍 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) |
12 | 11 | a1i 11 |
. 2
⊢ (𝐶 ≠ ∅ → (𝑍 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
13 | | eliuniin2.1 |
. . . 4
⊢
Ⅎ𝑥𝐶 |
14 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑥∅ |
15 | 13, 14 | nfne 2882 |
. . 3
⊢
Ⅎ𝑥 𝐶 ≠ ∅ |
16 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑥 𝑍 ∈ 𝐴 |
17 | | simp2 1055 |
. . . . . . 7
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑥 ∈ 𝐵) |
18 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐶 ≠ ∅ ∧
∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) |
19 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ ∅ → 𝐶 ≠ ∅) |
20 | | eliin2 38330 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ ∅ → (𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝐶 ≠ ∅ → (𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐶 ≠ ∅ ∧
∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → (𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
23 | 18, 22 | mpbird 246 |
. . . . . . . 8
⊢ ((𝐶 ≠ ∅ ∧
∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
24 | 23 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
25 | | rspe 2986 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) → ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
26 | 17, 24, 25 | syl2anc 691 |
. . . . . 6
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
27 | 26, 4 | sylibr 223 |
. . . . 5
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ ∪
𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷) |
28 | 27, 2 | sylibr 223 |
. . . 4
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ 𝐴) |
29 | 28 | 3exp 1256 |
. . 3
⊢ (𝐶 ≠ ∅ → (𝑥 ∈ 𝐵 → (∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴))) |
30 | 15, 16, 29 | rexlimd 3008 |
. 2
⊢ (𝐶 ≠ ∅ →
(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴)) |
31 | 12, 30 | impbid 201 |
1
⊢ (𝐶 ≠ ∅ → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |