Step | Hyp | Ref
| Expression |
1 | | difeq2 4051 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ∖ 𝑥) = (𝐴 ∖ ∅)) |
2 | | dif0 4306 |
. . . . . 6
⊢ (𝐴 ∖ ∅) = 𝐴 |
3 | 1, 2 | eqtrdi 2794 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 ∖ 𝑥) = 𝐴) |
4 | 3 | breq1d 5084 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐴 ∖ 𝑥) ≈ 𝐴 ↔ 𝐴 ≈ 𝐴)) |
5 | 4 | imbi2d 341 |
. . 3
⊢ (𝑥 = ∅ → ((ω
≼ 𝐴 → (𝐴 ∖ 𝑥) ≈ 𝐴) ↔ (ω ≼ 𝐴 → 𝐴 ≈ 𝐴))) |
6 | | difeq2 4051 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑦)) |
7 | 6 | breq1d 5084 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 ∖ 𝑥) ≈ 𝐴 ↔ (𝐴 ∖ 𝑦) ≈ 𝐴)) |
8 | 7 | imbi2d 341 |
. . 3
⊢ (𝑥 = 𝑦 → ((ω ≼ 𝐴 → (𝐴 ∖ 𝑥) ≈ 𝐴) ↔ (ω ≼ 𝐴 → (𝐴 ∖ 𝑦) ≈ 𝐴))) |
9 | | difeq2 4051 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑦 ∪ {𝑧}))) |
10 | | difun1 4223 |
. . . . . 6
⊢ (𝐴 ∖ (𝑦 ∪ {𝑧})) = ((𝐴 ∖ 𝑦) ∖ {𝑧}) |
11 | 9, 10 | eqtrdi 2794 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ∖ 𝑥) = ((𝐴 ∖ 𝑦) ∖ {𝑧})) |
12 | 11 | breq1d 5084 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∖ 𝑥) ≈ 𝐴 ↔ ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴)) |
13 | 12 | imbi2d 341 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((ω ≼ 𝐴 → (𝐴 ∖ 𝑥) ≈ 𝐴) ↔ (ω ≼ 𝐴 → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴))) |
14 | | difeq2 4051 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝐵)) |
15 | 14 | breq1d 5084 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐴 ∖ 𝑥) ≈ 𝐴 ↔ (𝐴 ∖ 𝐵) ≈ 𝐴)) |
16 | 15 | imbi2d 341 |
. . 3
⊢ (𝑥 = 𝐵 → ((ω ≼ 𝐴 → (𝐴 ∖ 𝑥) ≈ 𝐴) ↔ (ω ≼ 𝐴 → (𝐴 ∖ 𝐵) ≈ 𝐴))) |
17 | | reldom 8739 |
. . . . 5
⊢ Rel
≼ |
18 | 17 | brrelex2i 5644 |
. . . 4
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) |
19 | | enrefg 8772 |
. . . 4
⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (ω
≼ 𝐴 → 𝐴 ≈ 𝐴) |
21 | | domen2 8907 |
. . . . . . . . 9
⊢ ((𝐴 ∖ 𝑦) ≈ 𝐴 → (ω ≼ (𝐴 ∖ 𝑦) ↔ ω ≼ 𝐴)) |
22 | 21 | biimparc 480 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ (𝐴 ∖ 𝑦) ≈ 𝐴) → ω ≼ (𝐴 ∖ 𝑦)) |
23 | | infdifsn 9415 |
. . . . . . . 8
⊢ (ω
≼ (𝐴 ∖ 𝑦) → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ (𝐴 ∖ 𝑦)) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ (𝐴 ∖ 𝑦) ≈ 𝐴) → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ (𝐴 ∖ 𝑦)) |
25 | | entr 8792 |
. . . . . . 7
⊢ ((((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ (𝐴 ∖ 𝑦) ∧ (𝐴 ∖ 𝑦) ≈ 𝐴) → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴) |
26 | 24, 25 | sylancom 588 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ (𝐴 ∖ 𝑦) ≈ 𝐴) → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴) |
27 | 26 | ex 413 |
. . . . 5
⊢ (ω
≼ 𝐴 → ((𝐴 ∖ 𝑦) ≈ 𝐴 → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴)) |
28 | 27 | a2i 14 |
. . . 4
⊢ ((ω
≼ 𝐴 → (𝐴 ∖ 𝑦) ≈ 𝐴) → (ω ≼ 𝐴 → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴)) |
29 | 28 | a1i 11 |
. . 3
⊢ (𝑦 ∈ Fin → ((ω
≼ 𝐴 → (𝐴 ∖ 𝑦) ≈ 𝐴) → (ω ≼ 𝐴 → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴))) |
30 | 5, 8, 13, 16, 20, 29 | findcard2 8947 |
. 2
⊢ (𝐵 ∈ Fin → (ω
≼ 𝐴 → (𝐴 ∖ 𝐵) ≈ 𝐴)) |
31 | 30 | impcom 408 |
1
⊢ ((ω
≼ 𝐴 ∧ 𝐵 ∈ Fin) → (𝐴 ∖ 𝐵) ≈ 𝐴) |