Proof of Theorem findsg
| Step | Hyp | Ref
| Expression |
| 1 | | sseq2 4010 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅)) |
| 2 | 1 | adantl 481 |
. . . . . 6
⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅)) |
| 3 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (𝑥 = 𝐵 ↔ 𝑥 = ∅)) |
| 4 | | findsg.1 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) |
| 5 | 3, 4 | biimtrrdi 254 |
. . . . . . 7
⊢ (𝐵 = ∅ → (𝑥 = ∅ → (𝜑 ↔ 𝜓))) |
| 6 | 5 | imp 406 |
. . . . . 6
⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑 ↔ 𝜓)) |
| 7 | 2, 6 | imbi12d 344 |
. . . . 5
⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) |
| 8 | 1 | imbi1d 341 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑))) |
| 9 | | ss0 4402 |
. . . . . . . . 9
⊢ (𝐵 ⊆ ∅ → 𝐵 = ∅) |
| 10 | 9 | con3i 154 |
. . . . . . . 8
⊢ (¬
𝐵 = ∅ → ¬
𝐵 ⊆
∅) |
| 11 | 10 | pm2.21d 121 |
. . . . . . 7
⊢ (¬
𝐵 = ∅ → (𝐵 ⊆ ∅ → (𝜑 ↔ 𝜓))) |
| 12 | 11 | pm5.74d 273 |
. . . . . 6
⊢ (¬
𝐵 = ∅ → ((𝐵 ⊆ ∅ → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) |
| 13 | 8, 12 | sylan9bbr 510 |
. . . . 5
⊢ ((¬
𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) |
| 14 | 7, 13 | pm2.61ian 812 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) |
| 15 | 14 | imbi2d 340 |
. . 3
⊢ (𝑥 = ∅ → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ ∅ → 𝜓)))) |
| 16 | | sseq2 4010 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦)) |
| 17 | | findsg.2 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
| 18 | 16, 17 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝑦 → 𝜒))) |
| 19 | 18 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ 𝑦 → 𝜒)))) |
| 20 | | sseq2 4010 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ suc 𝑦)) |
| 21 | | findsg.3 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) |
| 22 | 20, 21 | imbi12d 344 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ suc 𝑦 → 𝜃))) |
| 23 | 22 | imbi2d 340 |
. . 3
⊢ (𝑥 = suc 𝑦 → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 24 | | sseq2 4010 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝐴)) |
| 25 | | findsg.4 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
| 26 | 24, 25 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝐴 → 𝜏))) |
| 27 | 26 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ 𝐴 → 𝜏)))) |
| 28 | | findsg.5 |
. . . 4
⊢ (𝐵 ∈ ω → 𝜓) |
| 29 | 28 | a1d 25 |
. . 3
⊢ (𝐵 ∈ ω → (𝐵 ⊆ ∅ → 𝜓)) |
| 30 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
| 31 | 30 | sucex 7826 |
. . . . . . . . . . . . 13
⊢ suc 𝑦 ∈ V |
| 32 | 31 | eqvinc 3649 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵)) |
| 33 | 28, 4 | imbitrrid 246 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → (𝐵 ∈ ω → 𝜑)) |
| 34 | 21 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝑦 → (𝜑 → 𝜃)) |
| 35 | 33, 34 | sylan9r 508 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ ω → 𝜃)) |
| 36 | 35 | exlimiv 1930 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ ω → 𝜃)) |
| 37 | 32, 36 | sylbi 217 |
. . . . . . . . . . 11
⊢ (suc
𝑦 = 𝐵 → (𝐵 ∈ ω → 𝜃)) |
| 38 | 37 | eqcoms 2745 |
. . . . . . . . . 10
⊢ (𝐵 = suc 𝑦 → (𝐵 ∈ ω → 𝜃)) |
| 39 | 38 | imim2i 16 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ ω → 𝜃))) |
| 40 | 39 | a1d 25 |
. . . . . . . 8
⊢ ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ ω → 𝜃)))) |
| 41 | 40 | com4r 94 |
. . . . . . 7
⊢ (𝐵 ∈ ω → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 42 | 41 | adantl 481 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 43 | | df-ne 2941 |
. . . . . . . . 9
⊢ (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦) |
| 44 | 43 | anbi2i 623 |
. . . . . . . 8
⊢ ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) ↔ (𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦)) |
| 45 | | annim 403 |
. . . . . . . 8
⊢ ((𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦)) |
| 46 | 44, 45 | bitri 275 |
. . . . . . 7
⊢ ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦)) |
| 47 | | nnon 7893 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
| 48 | | nnon 7893 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
| 49 | | onsssuc 6474 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ 𝐵 ∈ suc 𝑦)) |
| 50 | | onsuc 7831 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
| 51 | | onelpss 6424 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) |
| 52 | 50, 51 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) |
| 53 | 49, 52 | bitrd 279 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) |
| 54 | 47, 48, 53 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) |
| 55 | | findsg.6 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) |
| 56 | 55 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 ⊆ 𝑦 → (𝜒 → 𝜃))) |
| 57 | 56 | a1ddd 80 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 ⊆ 𝑦 → (𝜒 → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 58 | 57 | a2d 29 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ 𝑦 → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 59 | 58 | com23 86 |
. . . . . . . 8
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 ⊆ 𝑦 → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 60 | 54, 59 | sylbird 260 |
. . . . . . 7
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 61 | 46, 60 | biimtrrid 243 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (¬
(𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 62 | 42, 61 | pm2.61d 179 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))) |
| 63 | 62 | ex 412 |
. . . 4
⊢ (𝑦 ∈ ω → (𝐵 ∈ ω → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 64 | 63 | a2d 29 |
. . 3
⊢ (𝑦 ∈ ω → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ∈ ω → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
| 65 | 15, 19, 23, 27, 29, 64 | finds 7918 |
. 2
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐵 ⊆ 𝐴 → 𝜏))) |
| 66 | 65 | imp31 417 |
1
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏) |