Step | Hyp | Ref
| Expression |
1 | | ssid 3923 |
. . 3
⊢ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) |
2 | | simpr 488 |
. . . . 5
⊢ ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ¬ (𝑎 ∩ 𝑥) = ∅) |
3 | 2 | a1i 11 |
. . . 4
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ¬ (𝑎 ∩ 𝑥) = ∅)) |
4 | | df-ne 2941 |
. . . 4
⊢ ((𝑎 ∩ 𝑥) ≠ ∅ ↔ ¬ (𝑎 ∩ 𝑥) = ∅) |
5 | 3, 4 | syl6ibr 255 |
. . 3
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → (𝑎 ∩ 𝑥) ≠ ∅)) |
6 | | pm3.2 473 |
. . 3
⊢ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) → ((𝑎 ∩ 𝑥) ≠ ∅ → ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))) |
7 | 1, 5, 6 | mpsylsyld 69 |
. 2
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))) |
8 | | vex 3412 |
. . . . 5
⊢ 𝑥 ∈ V |
9 | 8 | inex2 5211 |
. . . 4
⊢ (𝑎 ∩ 𝑥) ∈ V |
10 | | inss2 4144 |
. . . . . . 7
⊢ (𝑎 ∩ 𝑥) ⊆ 𝑥 |
11 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → 𝑎 ⊆ On) |
12 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → 𝑥 ∈ 𝑎) |
13 | | ssel 3893 |
. . . . . . . . . 10
⊢ (𝑎 ⊆ On → (𝑥 ∈ 𝑎 → 𝑥 ∈ On)) |
14 | 11, 12, 13 | syl2im 40 |
. . . . . . . . 9
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → 𝑥 ∈ On)) |
15 | | eloni 6223 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → Ord 𝑥) |
16 | 14, 15 | syl6 35 |
. . . . . . . 8
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → Ord 𝑥)) |
17 | | ordwe 6226 |
. . . . . . . 8
⊢ (Ord
𝑥 → E We 𝑥) |
18 | 16, 17 | syl6 35 |
. . . . . . 7
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → E We 𝑥)) |
19 | | wess 5538 |
. . . . . . 7
⊢ ((𝑎 ∩ 𝑥) ⊆ 𝑥 → ( E We 𝑥 → E We (𝑎 ∩ 𝑥))) |
20 | 10, 18, 19 | mpsylsyld 69 |
. . . . . 6
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → E We (𝑎 ∩ 𝑥))) |
21 | | wefr 5541 |
. . . . . 6
⊢ ( E We
(𝑎 ∩ 𝑥) → E Fr (𝑎 ∩ 𝑥)) |
22 | 20, 21 | syl6 35 |
. . . . 5
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → E Fr (𝑎 ∩ 𝑥))) |
23 | | dfepfr 5536 |
. . . . 5
⊢ ( E Fr
(𝑎 ∩ 𝑥) ↔ ∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)) |
24 | 22, 23 | syl6ib 254 |
. . . 4
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))) |
25 | | spsbc 3707 |
. . . 4
⊢ ((𝑎 ∩ 𝑥) ∈ V → (∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) → [(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))) |
26 | 9, 24, 25 | mpsylsyld 69 |
. . 3
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → [(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))) |
27 | | onfrALTlem5 41835 |
. . 3
⊢
([(𝑎 ∩
𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)) |
28 | 26, 27 | syl6ib 254 |
. 2
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))) |
29 | 7, 28 | mpdd 43 |
1
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)) |