Step | Hyp | Ref
| Expression |
1 | | dfepfr 5536 |
. 2
⊢ ( E Fr On
↔ ∀𝑥((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
2 | | n0 4261 |
. . . 4
⊢ (𝑥 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) |
3 | | ineq2 4121 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑥 ∩ 𝑧) = (𝑥 ∩ 𝑦)) |
4 | 3 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → ((𝑥 ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑦) = ∅)) |
5 | 4 | rspcev 3537 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
6 | 5 | adantll 714 |
. . . . . . 7
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
7 | | inss1 4143 |
. . . . . . . 8
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥 |
8 | | ssel2 3895 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
9 | | eloni 6223 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → Ord 𝑦) |
10 | | ordfr 6228 |
. . . . . . . . . . 11
⊢ (Ord
𝑦 → E Fr 𝑦) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → E Fr 𝑦) |
12 | | inss2 4144 |
. . . . . . . . . . 11
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑦 |
13 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
14 | 13 | inex1 5210 |
. . . . . . . . . . . 12
⊢ (𝑥 ∩ 𝑦) ∈ V |
15 | 14 | epfrc 5537 |
. . . . . . . . . . 11
⊢ (( E Fr
𝑦 ∧ (𝑥 ∩ 𝑦) ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) |
16 | 12, 15 | mp3an2 1451 |
. . . . . . . . . 10
⊢ (( E Fr
𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) |
17 | 11, 16 | sylan 583 |
. . . . . . . . 9
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) |
18 | | inass 4134 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ (𝑦 ∩ 𝑧)) |
19 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦) |
20 | | elinel2 4110 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝑥 ∩ 𝑦) → 𝑧 ∈ 𝑦) |
21 | | ordelss 6229 |
. . . . . . . . . . . . . . . 16
⊢ ((Ord
𝑦 ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑦) |
22 | 19, 20, 21 | syl2an 599 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → 𝑧 ⊆ 𝑦) |
23 | | sseqin2 4130 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ⊆ 𝑦 ↔ (𝑦 ∩ 𝑧) = 𝑧) |
24 | 22, 23 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑦 ∩ 𝑧) = 𝑧) |
25 | 24 | ineq2d 4127 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑥 ∩ (𝑦 ∩ 𝑧)) = (𝑥 ∩ 𝑧)) |
26 | 18, 25 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ 𝑧)) |
27 | 26 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑧) = ∅)) |
28 | 27 | rexbidva 3215 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)) |
29 | 28 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)) |
30 | 17, 29 | mpbid 235 |
. . . . . . . 8
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅) |
31 | | ssrexv 3968 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ⊆ 𝑥 → (∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
32 | 7, 30, 31 | mpsyl 68 |
. . . . . . 7
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
33 | 6, 32 | pm2.61dane 3029 |
. . . . . 6
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
34 | 33 | ex 416 |
. . . . 5
⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
35 | 34 | exlimdv 1941 |
. . . 4
⊢ (𝑥 ⊆ On → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
36 | 2, 35 | syl5bi 245 |
. . 3
⊢ (𝑥 ⊆ On → (𝑥 ≠ ∅ →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
37 | 36 | imp 410 |
. 2
⊢ ((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
38 | 1, 37 | mpgbir 1807 |
1
⊢ E Fr
On |