Step | Hyp | Ref
| Expression |
1 | | eleq1w 2218 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦)) |
2 | | equequ1 1692 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦)) |
3 | | eleq2 2221 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧)) |
4 | 1, 2, 3 | 3orbi123d 1293 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) |
5 | 4 | ralbidv 2457 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) |
6 | 5 | imbi2d 229 |
. . . 4
⊢ (𝑥 = 𝑧 → ((EXMID →
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) ↔ (EXMID →
∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧)))) |
7 | | simplll 523 |
. . . . . . . 8
⊢ ((((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) ∧ 𝑎 ∈ On) → 𝑥 ∈ On) |
8 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) ∧ 𝑎 ∈ On) → 𝑎 ∈ On) |
9 | | simplr 520 |
. . . . . . . 8
⊢ ((((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) ∧ 𝑎 ∈ On) →
EXMID) |
10 | | simpllr 524 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) ∧ 𝑎 ∈ On) → ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) |
11 | | pm2.27 40 |
. . . . . . . . . . 11
⊢
(EXMID → ((EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧)) → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) |
12 | 11 | ralimdv 2525 |
. . . . . . . . . 10
⊢
(EXMID → (∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧)) → ∀𝑧 ∈ 𝑥 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) |
13 | 12 | ad2antlr 481 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) ∧ 𝑎 ∈ On) →
(∀𝑧 ∈ 𝑥 (EXMID →
∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧)) → ∀𝑧 ∈ 𝑥 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) |
14 | 10, 13 | mpd 13 |
. . . . . . . 8
⊢ ((((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) ∧ 𝑎 ∈ On) → ∀𝑧 ∈ 𝑥 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧)) |
15 | 7, 8, 9, 14 | exmidontriimlem4 7161 |
. . . . . . 7
⊢ ((((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) ∧ 𝑎 ∈ On) → (𝑥 ∈ 𝑎 ∨ 𝑥 = 𝑎 ∨ 𝑎 ∈ 𝑥)) |
16 | 15 | ralrimiva 2530 |
. . . . . 6
⊢ (((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) →
∀𝑎 ∈ On (𝑥 ∈ 𝑎 ∨ 𝑥 = 𝑎 ∨ 𝑎 ∈ 𝑥)) |
17 | | eleq2 2221 |
. . . . . . . 8
⊢ (𝑎 = 𝑦 → (𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝑦)) |
18 | | equequ2 1693 |
. . . . . . . 8
⊢ (𝑎 = 𝑦 → (𝑥 = 𝑎 ↔ 𝑥 = 𝑦)) |
19 | | eleq1w 2218 |
. . . . . . . 8
⊢ (𝑎 = 𝑦 → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
20 | 17, 18, 19 | 3orbi123d 1293 |
. . . . . . 7
⊢ (𝑎 = 𝑦 → ((𝑥 ∈ 𝑎 ∨ 𝑥 = 𝑎 ∨ 𝑎 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))) |
21 | 20 | cbvralv 2680 |
. . . . . 6
⊢
(∀𝑎 ∈ On
(𝑥 ∈ 𝑎 ∨ 𝑥 = 𝑎 ∨ 𝑎 ∈ 𝑥) ↔ ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
22 | 16, 21 | sylib 121 |
. . . . 5
⊢ (((𝑥 ∈ On ∧ ∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))) ∧ EXMID) →
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
23 | 22 | exp31 362 |
. . . 4
⊢ (𝑥 ∈ On → (∀𝑧 ∈ 𝑥 (EXMID → ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧)) → (EXMID →
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))) |
24 | 6, 23 | tfis2 4546 |
. . 3
⊢ (𝑥 ∈ On →
(EXMID → ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))) |
25 | 24 | impcom 124 |
. 2
⊢
((EXMID ∧ 𝑥 ∈ On) → ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
26 | 25 | ralrimiva 2530 |
1
⊢
(EXMID → ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |