Proof of Theorem tfindsg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sseq2 4009 | . . . . . . 7
⊢ (𝑥 = ∅ → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅)) | 
| 2 | 1 | adantl 481 | . . . . . 6
⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅)) | 
| 3 |  | eqeq2 2748 | . . . . . . . 8
⊢ (𝐵 = ∅ → (𝑥 = 𝐵 ↔ 𝑥 = ∅)) | 
| 4 |  | tfindsg.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 4401 | . . . . . . . . 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 811 | . . . 4
⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) | 
| 15 | 14 | imbi2d 340 | . . 3
⊢ (𝑥 = ∅ → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓)))) | 
| 16 |  | sseq2 4009 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦)) | 
| 17 |  | tfindsg.2 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | 
| 18 | 16, 17 | imbi12d 344 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝑦 → 𝜒))) | 
| 19 | 18 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)))) | 
| 20 |  | sseq2 4009 | . . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ suc 𝑦)) | 
| 21 |  | tfindsg.3 | . . . . 5
⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) | 
| 22 | 20, 21 | imbi12d 344 | . . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ suc 𝑦 → 𝜃))) | 
| 23 | 22 | imbi2d 340 | . . 3
⊢ (𝑥 = suc 𝑦 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 24 |  | sseq2 4009 | . . . . 5
⊢ (𝑥 = 𝐴 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝐴)) | 
| 25 |  | tfindsg.4 | . . . . 5
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | 
| 26 | 24, 25 | imbi12d 344 | . . . 4
⊢ (𝑥 = 𝐴 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝐴 → 𝜏))) | 
| 27 | 26 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ 𝐴 → 𝜏)))) | 
| 28 |  | tfindsg.5 | . . . 4
⊢ (𝐵 ∈ On → 𝜓) | 
| 29 | 28 | a1d 25 | . . 3
⊢ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓)) | 
| 30 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V | 
| 31 | 30 | sucex 7827 | . . . . . . . . . . . . 13
⊢ suc 𝑦 ∈ V | 
| 32 | 31 | eqvinc 3648 | . . . . . . . . . . . 12
⊢ (suc
𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵)) | 
| 33 | 28, 4 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → (𝐵 ∈ On → 𝜑)) | 
| 34 | 21 | biimpd 229 | . . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝑦 → (𝜑 → 𝜃)) | 
| 35 | 33, 34 | sylan9r 508 | . . . . . . . . . . . . 13
⊢ ((𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃)) | 
| 36 | 35 | exlimiv 1929 | . . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃)) | 
| 37 | 32, 36 | sylbi 217 | . . . . . . . . . . 11
⊢ (suc
𝑦 = 𝐵 → (𝐵 ∈ On → 𝜃)) | 
| 38 | 37 | eqcoms 2744 | . . . . . . . . . 10
⊢ (𝐵 = suc 𝑦 → (𝐵 ∈ On → 𝜃)) | 
| 39 | 38 | imim2i 16 | . . . . . . . . 9
⊢ ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ On → 𝜃))) | 
| 40 | 39 | a1d 25 | . . . . . . . 8
⊢ ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ On → 𝜃)))) | 
| 41 | 40 | com4r 94 | . . . . . . 7
⊢ (𝐵 ∈ On → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 42 | 41 | adantl 481 | . . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 43 |  | df-ne 2940 | . . . . . . . . 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 |  | onsssuc 6473 | . . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ 𝐵 ∈ suc 𝑦)) | 
| 48 |  | onsuc 7832 | . . . . . . . . . . 11
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) | 
| 49 |  | onelpss 6423 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) | 
| 50 | 48, 49 | sylan2 593 | . . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) | 
| 51 | 47, 50 | bitrd 279 | . . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) | 
| 52 | 51 | ancoms 458 | . . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) | 
| 53 |  | tfindsg.6 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) | 
| 54 | 53 | ex 412 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 → (𝜒 → 𝜃))) | 
| 55 | 54 | a1ddd 80 | . . . . . . . . . 10
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 → (𝜒 → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 56 | 55 | a2d 29 | . . . . . . . . 9
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ 𝑦 → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 57 | 56 | com23 86 | . . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 58 | 52, 57 | sylbird 260 | . . . . . . 7
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 59 | 46, 58 | biimtrrid 243 | . . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 60 | 42, 59 | pm2.61d 179 | . . . . 5
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))) | 
| 61 | 60 | ex 412 | . . . 4
⊢ (𝑦 ∈ On → (𝐵 ∈ On → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 62 | 61 | a2d 29 | . . 3
⊢ (𝑦 ∈ On → ((𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦 → 𝜃)))) | 
| 63 |  | pm2.27 42 | . . . . . . . . 9
⊢ (𝐵 ∈ On → ((𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ⊆ 𝑦 → 𝜒))) | 
| 64 | 63 | ralimdv 3168 | . . . . . . . 8
⊢ (𝐵 ∈ On → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → ∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒))) | 
| 65 | 64 | ad2antlr 727 | . . . . . . 7
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → ∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒))) | 
| 66 |  | tfindsg.7 | . . . . . . 7
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)) | 
| 67 | 65, 66 | syld 47 | . . . . . 6
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → 𝜑)) | 
| 68 | 67 | exp31 419 | . . . . 5
⊢ (Lim
𝑥 → (𝐵 ∈ On → (𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → 𝜑)))) | 
| 69 | 68 | com3l 89 | . . . 4
⊢ (𝐵 ∈ On → (𝐵 ⊆ 𝑥 → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → 𝜑)))) | 
| 70 | 69 | com4t 93 | . . 3
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)))) | 
| 71 | 15, 19, 23, 27, 29, 62, 70 | tfinds 7882 | . 2
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐵 ⊆ 𝐴 → 𝜏))) | 
| 72 | 71 | imp31 417 | 1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → 𝜏) |