Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
⊢ ∅ ∈ V |
2 |
|
eleq1 |
⊢ ( ∩ 𝐴 = ∅ → ( ∩ 𝐴 ∈ V ↔ ∅ ∈ V ) ) |
3 |
1 2
|
mpbiri |
⊢ ( ∩ 𝐴 = ∅ → ∩ 𝐴 ∈ V ) |
4 |
|
intex |
⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V ) |
5 |
3 4
|
sylibr |
⊢ ( ∩ 𝐴 = ∅ → 𝐴 ≠ ∅ ) |
6 |
|
onint |
⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 ) |
7 |
5 6
|
sylan2 |
⊢ ( ( 𝐴 ⊆ On ∧ ∩ 𝐴 = ∅ ) → ∩ 𝐴 ∈ 𝐴 ) |
8 |
|
eleq1 |
⊢ ( ∩ 𝐴 = ∅ → ( ∩ 𝐴 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) ) |
9 |
8
|
adantl |
⊢ ( ( 𝐴 ⊆ On ∧ ∩ 𝐴 = ∅ ) → ( ∩ 𝐴 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) ) |
10 |
7 9
|
mpbid |
⊢ ( ( 𝐴 ⊆ On ∧ ∩ 𝐴 = ∅ ) → ∅ ∈ 𝐴 ) |
11 |
10
|
ex |
⊢ ( 𝐴 ⊆ On → ( ∩ 𝐴 = ∅ → ∅ ∈ 𝐴 ) ) |
12 |
|
int0el |
⊢ ( ∅ ∈ 𝐴 → ∩ 𝐴 = ∅ ) |
13 |
11 12
|
impbid1 |
⊢ ( 𝐴 ⊆ On → ( ∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴 ) ) |