Step |
Hyp |
Ref |
Expression |
1 |
|
dfepfr |
⊢ ( E Fr On ↔ ∀ 𝑎 ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) |
2 |
|
simpr |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → 𝑎 ≠ ∅ ) |
3 |
|
n0 |
⊢ ( 𝑎 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑎 ) |
4 |
|
onfrALTlem1 |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) |
5 |
4
|
expd |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( 𝑥 ∈ 𝑎 → ( ( 𝑎 ∩ 𝑥 ) = ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) ) |
6 |
|
onfrALTlem2 |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) |
7 |
6
|
expd |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( 𝑥 ∈ 𝑎 → ( ¬ ( 𝑎 ∩ 𝑥 ) = ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) ) |
8 |
|
pm2.61 |
⊢ ( ( ( 𝑎 ∩ 𝑥 ) = ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) → ( ( ¬ ( 𝑎 ∩ 𝑥 ) = ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) |
9 |
5 7 8
|
syl6c |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) |
10 |
9
|
exlimdv |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ∃ 𝑥 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) |
11 |
3 10
|
syl5bi |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( 𝑎 ≠ ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) |
12 |
2 11
|
mpd |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) |
13 |
1 12
|
mpgbir |
⊢ E Fr On |