Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ On) |
2 | 1 | sselda 3981 |
. . . . . . . 8
⊢ (((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
3 | | ssel2 3976 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ On) |
5 | | ontri1 6395 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦)) |
6 | 2, 4, 5 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦)) |
7 | 6 | ralbidva 3175 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦)) |
8 | 7 | rexbidva 3176 |
. . . . 5
⊢ (𝐴 ⊆ On → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦)) |
9 | 8 | notbid 317 |
. . . 4
⊢ (𝐴 ⊆ On → (¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦)) |
10 | 9 | bicomd 222 |
. . 3
⊢ (𝐴 ⊆ On → (¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
11 | | dfrex2 3073 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 𝑥 ∈ 𝑦 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦) |
12 | 11 | ralbii 3093 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦) |
13 | | ralnex 3072 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦) |
14 | 12, 13 | bitri 274 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦) |
15 | | unielid 41953 |
. . . 4
⊢ (∪ 𝐴
∈ 𝐴 ↔
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥) |
16 | 15 | notbii 319 |
. . 3
⊢ (¬
∪ 𝐴 ∈ 𝐴 ↔ ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥) |
17 | 10, 14, 16 | 3bitr4g 313 |
. 2
⊢ (𝐴 ⊆ On →
(∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ¬ ∪
𝐴 ∈ 𝐴)) |
18 | | onsupnmax 41962 |
. . 3
⊢ (𝐴 ⊆ On → (¬ ∪ 𝐴
∈ 𝐴 → ∪ 𝐴 =
∪ ∪ 𝐴)) |
19 | 18 | pm4.71rd 563 |
. 2
⊢ (𝐴 ⊆ On → (¬ ∪ 𝐴
∈ 𝐴 ↔ (∪ 𝐴 =
∪ ∪ 𝐴 ∧ ¬ ∪
𝐴 ∈ 𝐴))) |
20 | 17, 19 | bitrd 278 |
1
⊢ (𝐴 ⊆ On →
(∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ (∪ 𝐴 = ∪
∪ 𝐴 ∧ ¬ ∪
𝐴 ∈ 𝐴))) |