Step |
Hyp |
Ref |
Expression |
1 |
|
onint |
⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ∩ 𝐵 ∈ 𝐵 ) |
2 |
|
eleq1 |
⊢ ( 𝐴 = ∩ 𝐵 → ( 𝐴 ∈ 𝐵 ↔ ∩ 𝐵 ∈ 𝐵 ) ) |
3 |
1 2
|
syl5ibrcom |
⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 → 𝐴 ∈ 𝐵 ) ) |
4 |
|
eleq2 |
⊢ ( 𝐴 = ∩ 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ∩ 𝐵 ) ) |
5 |
4
|
biimpd |
⊢ ( 𝐴 = ∩ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∩ 𝐵 ) ) |
6 |
|
onnmin |
⊢ ( ( 𝐵 ⊆ On ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ∩ 𝐵 ) |
7 |
6
|
ex |
⊢ ( 𝐵 ⊆ On → ( 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ ∩ 𝐵 ) ) |
8 |
7
|
con2d |
⊢ ( 𝐵 ⊆ On → ( 𝑥 ∈ ∩ 𝐵 → ¬ 𝑥 ∈ 𝐵 ) ) |
9 |
5 8
|
syl9r |
⊢ ( 𝐵 ⊆ On → ( 𝐴 = ∩ 𝐵 → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ) ) |
10 |
9
|
ralrimdv |
⊢ ( 𝐵 ⊆ On → ( 𝐴 = ∩ 𝐵 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) ) |
11 |
10
|
adantr |
⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) ) |
12 |
3 11
|
jcad |
⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 → ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) ) ) |
13 |
|
oneqmini |
⊢ ( 𝐵 ⊆ On → ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) → 𝐴 = ∩ 𝐵 ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) → 𝐴 = ∩ 𝐵 ) ) |
15 |
12 14
|
impbid |
⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) ) ) |