Step |
Hyp |
Ref |
Expression |
1 |
|
ssid |
⊢ ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) |
2 |
|
simpr |
⊢ ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) |
3 |
2
|
a1i |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) ) |
4 |
|
df-ne |
⊢ ( ( 𝑎 ∩ 𝑥 ) ≠ ∅ ↔ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) |
5 |
3 4
|
syl6ibr |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) ) |
6 |
|
pm3.2 |
⊢ ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) → ( ( 𝑎 ∩ 𝑥 ) ≠ ∅ → ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) ) ) |
7 |
1 5 6
|
mpsylsyld |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) ) ) |
8 |
|
vex |
⊢ 𝑥 ∈ V |
9 |
8
|
inex2 |
⊢ ( 𝑎 ∩ 𝑥 ) ∈ V |
10 |
|
inss2 |
⊢ ( 𝑎 ∩ 𝑥 ) ⊆ 𝑥 |
11 |
|
simpl |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → 𝑎 ⊆ On ) |
12 |
|
simpl |
⊢ ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → 𝑥 ∈ 𝑎 ) |
13 |
|
ssel |
⊢ ( 𝑎 ⊆ On → ( 𝑥 ∈ 𝑎 → 𝑥 ∈ On ) ) |
14 |
11 12 13
|
syl2im |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → 𝑥 ∈ On ) ) |
15 |
|
eloni |
⊢ ( 𝑥 ∈ On → Ord 𝑥 ) |
16 |
14 15
|
syl6 |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → Ord 𝑥 ) ) |
17 |
|
ordwe |
⊢ ( Ord 𝑥 → E We 𝑥 ) |
18 |
16 17
|
syl6 |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → E We 𝑥 ) ) |
19 |
|
wess |
⊢ ( ( 𝑎 ∩ 𝑥 ) ⊆ 𝑥 → ( E We 𝑥 → E We ( 𝑎 ∩ 𝑥 ) ) ) |
20 |
10 18 19
|
mpsylsyld |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → E We ( 𝑎 ∩ 𝑥 ) ) ) |
21 |
|
wefr |
⊢ ( E We ( 𝑎 ∩ 𝑥 ) → E Fr ( 𝑎 ∩ 𝑥 ) ) |
22 |
20 21
|
syl6 |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → E Fr ( 𝑎 ∩ 𝑥 ) ) ) |
23 |
|
dfepfr |
⊢ ( E Fr ( 𝑎 ∩ 𝑥 ) ↔ ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ) |
24 |
22 23
|
syl6ib |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ) ) |
25 |
|
spsbc |
⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ) ) |
26 |
9 24 25
|
mpsylsyld |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ) ) |
27 |
|
onfrALTlem5 |
⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) |
28 |
26 27
|
syl6ib |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) ) |
29 |
7 28
|
mpdd |
⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) |