Step | Hyp | Ref
| Expression |
1 | | treq 5142 |
. . 3
⊢ (𝑧 = 𝑤 → (Tr 𝑧 ↔ Tr 𝑤)) |
2 | | neeq1 3049 |
. . 3
⊢ (𝑧 = 𝑤 → (𝑧 ≠ ∅ ↔ 𝑤 ≠ ∅)) |
3 | | eleq2 2878 |
. . . . 5
⊢ (𝑧 = 𝑤 → (∪ 𝑥 ∈ 𝑧 ↔ ∪ 𝑥 ∈ 𝑤)) |
4 | | eleq2 2878 |
. . . . 5
⊢ (𝑧 = 𝑤 → (𝒫 𝑥 ∈ 𝑧 ↔ 𝒫 𝑥 ∈ 𝑤)) |
5 | | eleq2 2878 |
. . . . . 6
⊢ (𝑧 = 𝑤 → ({𝑥, 𝑦} ∈ 𝑧 ↔ {𝑥, 𝑦} ∈ 𝑤)) |
6 | 5 | raleqbi1dv 3356 |
. . . . 5
⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧 ↔ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤)) |
7 | 3, 4, 6 | 3anbi123d 1433 |
. . . 4
⊢ (𝑧 = 𝑤 → ((∪ 𝑥 ∈ 𝑧 ∧ 𝒫 𝑥 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧) ↔ (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤))) |
8 | 7 | raleqbi1dv 3356 |
. . 3
⊢ (𝑧 = 𝑤 → (∀𝑥 ∈ 𝑧 (∪ 𝑥 ∈ 𝑧 ∧ 𝒫 𝑥 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧) ↔ ∀𝑥 ∈ 𝑤 (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤))) |
9 | 1, 2, 8 | 3anbi123d 1433 |
. 2
⊢ (𝑧 = 𝑤 → ((Tr 𝑧 ∧ 𝑧 ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 (∪ 𝑥 ∈ 𝑧 ∧ 𝒫 𝑥 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧)) ↔ (Tr 𝑤 ∧ 𝑤 ≠ ∅ ∧ ∀𝑥 ∈ 𝑤 (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤)))) |
10 | | treq 5142 |
. . 3
⊢ (𝑤 = 𝑈 → (Tr 𝑤 ↔ Tr 𝑈)) |
11 | | neeq1 3049 |
. . 3
⊢ (𝑤 = 𝑈 → (𝑤 ≠ ∅ ↔ 𝑈 ≠ ∅)) |
12 | | eleq2 2878 |
. . . . 5
⊢ (𝑤 = 𝑈 → (∪ 𝑥 ∈ 𝑤 ↔ ∪ 𝑥 ∈ 𝑈)) |
13 | | eleq2 2878 |
. . . . 5
⊢ (𝑤 = 𝑈 → (𝒫 𝑥 ∈ 𝑤 ↔ 𝒫 𝑥 ∈ 𝑈)) |
14 | | eleq2 2878 |
. . . . . 6
⊢ (𝑤 = 𝑈 → ({𝑥, 𝑦} ∈ 𝑤 ↔ {𝑥, 𝑦} ∈ 𝑈)) |
15 | 14 | raleqbi1dv 3356 |
. . . . 5
⊢ (𝑤 = 𝑈 → (∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤 ↔ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈)) |
16 | 12, 13, 15 | 3anbi123d 1433 |
. . . 4
⊢ (𝑤 = 𝑈 → ((∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤) ↔ (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))) |
17 | 16 | raleqbi1dv 3356 |
. . 3
⊢ (𝑤 = 𝑈 → (∀𝑥 ∈ 𝑤 (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤) ↔ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))) |
18 | 10, 11, 17 | 3anbi123d 1433 |
. 2
⊢ (𝑤 = 𝑈 → ((Tr 𝑤 ∧ 𝑤 ≠ ∅ ∧ ∀𝑥 ∈ 𝑤 (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤)) ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈)))) |
19 | | df-wun 10113 |
. 2
⊢ WUni =
{𝑧 ∣ (Tr 𝑧 ∧ 𝑧 ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 (∪ 𝑥 ∈ 𝑧 ∧ 𝒫 𝑥 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧))} |
20 | 9, 18, 19 | elab2gw 3613 |
1
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈)))) |