Proof of Theorem eliuniin
Step | Hyp | Ref
| Expression |
1 | | eliuniin.1 |
. . . . . . 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 | | simp2 1055 |
. . . . . . 7
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑥 ∈ 𝐵) |
14 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑍 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) |
15 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ 𝑉) |
16 | | eliin 4461 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑍 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → (𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
19 | 14, 18 | mpbird 246 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
20 | 19 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
21 | | rspe 2986 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) → ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
22 | 13, 20, 21 | syl2anc 691 |
. . . . . 6
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
23 | 22, 4 | sylibr 223 |
. . . . 5
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ ∪
𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷) |
24 | 23, 2 | sylibr 223 |
. . . 4
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ 𝐴) |
25 | 24 | 3exp 1256 |
. . 3
⊢ (𝑍 ∈ 𝑉 → (𝑥 ∈ 𝐵 → (∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴))) |
26 | 25 | rexlimdv 3012 |
. 2
⊢ (𝑍 ∈ 𝑉 → (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴)) |
27 | 12, 26 | impbid 201 |
1
⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |