Step | Hyp | Ref
| Expression |
1 | | eleq2 2228 |
. . 3
⊢ (𝑏 = 𝐵 → (𝐴 ∈ 𝑏 ↔ 𝐴 ∈ 𝐵)) |
2 | | eqeq2 2174 |
. . 3
⊢ (𝑏 = 𝐵 → (𝐴 = 𝑏 ↔ 𝐴 = 𝐵)) |
3 | | eleq1 2227 |
. . 3
⊢ (𝑏 = 𝐵 → (𝑏 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
4 | 1, 2, 3 | 3orbi123d 1300 |
. 2
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ 𝑏 ∨ 𝐴 = 𝑏 ∨ 𝑏 ∈ 𝐴) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
5 | | eleq2w 2226 |
. . . . . . 7
⊢ (𝑏 = 𝑤 → (𝐴 ∈ 𝑏 ↔ 𝐴 ∈ 𝑤)) |
6 | | eqeq2 2174 |
. . . . . . 7
⊢ (𝑏 = 𝑤 → (𝐴 = 𝑏 ↔ 𝐴 = 𝑤)) |
7 | | eleq1w 2225 |
. . . . . . 7
⊢ (𝑏 = 𝑤 → (𝑏 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
8 | 5, 6, 7 | 3orbi123d 1300 |
. . . . . 6
⊢ (𝑏 = 𝑤 → ((𝐴 ∈ 𝑏 ∨ 𝐴 = 𝑏 ∨ 𝑏 ∈ 𝐴) ↔ (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) |
9 | 8 | imbi2d 229 |
. . . . 5
⊢ (𝑏 = 𝑤 → ((𝜑 → (𝐴 ∈ 𝑏 ∨ 𝐴 = 𝑏 ∨ 𝑏 ∈ 𝐴)) ↔ (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴)))) |
10 | | exmidontriimlem4.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ On) |
11 | 10 | adantl 275 |
. . . . . . 7
⊢ (((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) → 𝐴 ∈ On) |
12 | | simpll 519 |
. . . . . . 7
⊢ (((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) → 𝑏 ∈ On) |
13 | | exmidontriimlem4.em |
. . . . . . . 8
⊢ (𝜑 →
EXMID) |
14 | 13 | adantl 275 |
. . . . . . 7
⊢ (((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) →
EXMID) |
15 | | exmidontriimlem4.h |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧)) |
16 | 15 | adantl 275 |
. . . . . . 7
⊢ (((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧)) |
17 | | simplr 520 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) ∧ 𝑣 ∈ 𝑏) → 𝜑) |
18 | | eleq2w 2226 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑣 → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑣)) |
19 | | eqeq2 2174 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑣 → (𝐴 = 𝑤 ↔ 𝐴 = 𝑣)) |
20 | | eleq1w 2225 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑣 → (𝑤 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴)) |
21 | 18, 19, 20 | 3orbi123d 1300 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑣 → ((𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴) ↔ (𝐴 ∈ 𝑣 ∨ 𝐴 = 𝑣 ∨ 𝑣 ∈ 𝐴))) |
22 | 21 | imbi2d 229 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑣 → ((𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴)) ↔ (𝜑 → (𝐴 ∈ 𝑣 ∨ 𝐴 = 𝑣 ∨ 𝑣 ∈ 𝐴)))) |
23 | | simpllr 524 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) ∧ 𝑣 ∈ 𝑏) → ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) |
24 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) ∧ 𝑣 ∈ 𝑏) → 𝑣 ∈ 𝑏) |
25 | 22, 23, 24 | rspcdva 2831 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) ∧ 𝑣 ∈ 𝑏) → (𝜑 → (𝐴 ∈ 𝑣 ∨ 𝐴 = 𝑣 ∨ 𝑣 ∈ 𝐴))) |
26 | 17, 25 | mpd 13 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) ∧ 𝑣 ∈ 𝑏) → (𝐴 ∈ 𝑣 ∨ 𝐴 = 𝑣 ∨ 𝑣 ∈ 𝐴)) |
27 | 26 | ralrimiva 2537 |
. . . . . . . 8
⊢ (((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) → ∀𝑣 ∈ 𝑏 (𝐴 ∈ 𝑣 ∨ 𝐴 = 𝑣 ∨ 𝑣 ∈ 𝐴)) |
28 | | eleq2w 2226 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑦 → (𝐴 ∈ 𝑣 ↔ 𝐴 ∈ 𝑦)) |
29 | | eqeq2 2174 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑦 → (𝐴 = 𝑣 ↔ 𝐴 = 𝑦)) |
30 | | eleq1w 2225 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
31 | 28, 29, 30 | 3orbi123d 1300 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → ((𝐴 ∈ 𝑣 ∨ 𝐴 = 𝑣 ∨ 𝑣 ∈ 𝐴) ↔ (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))) |
32 | 31 | cbvralv 2690 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑏 (𝐴 ∈ 𝑣 ∨ 𝐴 = 𝑣 ∨ 𝑣 ∈ 𝐴) ↔ ∀𝑦 ∈ 𝑏 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴)) |
33 | 27, 32 | sylib 121 |
. . . . . . 7
⊢ (((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) → ∀𝑦 ∈ 𝑏 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴)) |
34 | 11, 12, 14, 16, 33 | exmidontriimlem3 7171 |
. . . . . 6
⊢ (((𝑏 ∈ On ∧ ∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴))) ∧ 𝜑) → (𝐴 ∈ 𝑏 ∨ 𝐴 = 𝑏 ∨ 𝑏 ∈ 𝐴)) |
35 | 34 | exp31 362 |
. . . . 5
⊢ (𝑏 ∈ On → (∀𝑤 ∈ 𝑏 (𝜑 → (𝐴 ∈ 𝑤 ∨ 𝐴 = 𝑤 ∨ 𝑤 ∈ 𝐴)) → (𝜑 → (𝐴 ∈ 𝑏 ∨ 𝐴 = 𝑏 ∨ 𝑏 ∈ 𝐴)))) |
36 | 9, 35 | tfis2 4557 |
. . . 4
⊢ (𝑏 ∈ On → (𝜑 → (𝐴 ∈ 𝑏 ∨ 𝐴 = 𝑏 ∨ 𝑏 ∈ 𝐴))) |
37 | 36 | impcom 124 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ On) → (𝐴 ∈ 𝑏 ∨ 𝐴 = 𝑏 ∨ 𝑏 ∈ 𝐴)) |
38 | 37 | ralrimiva 2537 |
. 2
⊢ (𝜑 → ∀𝑏 ∈ On (𝐴 ∈ 𝑏 ∨ 𝐴 = 𝑏 ∨ 𝑏 ∈ 𝐴)) |
39 | | exmidontriimlem4.b |
. 2
⊢ (𝜑 → 𝐵 ∈ On) |
40 | 4, 38, 39 | rspcdva 2831 |
1
⊢ (𝜑 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |