Proof of Theorem tfindsg2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | onelon 6409 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | 
| 2 |  | onsucb 7837 | . . 3
⊢ (𝐵 ∈ On ↔ suc 𝐵 ∈ On) | 
| 3 | 1, 2 | sylib 218 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → suc 𝐵 ∈ On) | 
| 4 |  | eloni 6394 | . . . 4
⊢ (𝐴 ∈ On → Ord 𝐴) | 
| 5 |  | ordsucss 7838 | . . . 4
⊢ (Ord
𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴)) | 
| 6 | 4, 5 | syl 17 | . . 3
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴)) | 
| 7 | 6 | imp 406 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → suc 𝐵 ⊆ 𝐴) | 
| 8 |  | tfindsg2.1 | . . . . 5
⊢ (𝑥 = suc 𝐵 → (𝜑 ↔ 𝜓)) | 
| 9 |  | tfindsg2.2 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | 
| 10 |  | tfindsg2.3 | . . . . 5
⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) | 
| 11 |  | tfindsg2.4 | . . . . 5
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | 
| 12 |  | tfindsg2.5 | . . . . . 6
⊢ (𝐵 ∈ On → 𝜓) | 
| 13 | 2, 12 | sylbir 235 | . . . . 5
⊢ (suc
𝐵 ∈ On → 𝜓) | 
| 14 |  | eloni 6394 | . . . . . . . . . 10
⊢ (𝑦 ∈ On → Ord 𝑦) | 
| 15 |  | ordelsuc 7840 | . . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ Ord 𝑦) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) | 
| 16 | 14, 15 | sylan2 593 | . . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) | 
| 17 | 16 | ancoms 458 | . . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) | 
| 18 |  | tfindsg2.6 | . . . . . . . . . 10
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ 𝑦) → (𝜒 → 𝜃)) | 
| 19 | 18 | ex 412 | . . . . . . . . 9
⊢ (𝑦 ∈ On → (𝐵 ∈ 𝑦 → (𝜒 → 𝜃))) | 
| 20 | 19 | adantr 480 | . . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ∈ 𝑦 → (𝜒 → 𝜃))) | 
| 21 | 17, 20 | sylbird 260 | . . . . . . 7
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (suc 𝐵 ⊆ 𝑦 → (𝜒 → 𝜃))) | 
| 22 | 2, 21 | sylan2br 595 | . . . . . 6
⊢ ((𝑦 ∈ On ∧ suc 𝐵 ∈ On) → (suc 𝐵 ⊆ 𝑦 → (𝜒 → 𝜃))) | 
| 23 | 22 | imp 406 | . . . . 5
⊢ (((𝑦 ∈ On ∧ suc 𝐵 ∈ On) ∧ suc 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) | 
| 24 |  | tfindsg2.7 | . . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) | 
| 25 | 24 | ex 412 | . . . . . . . . 9
⊢ (Lim
𝑥 → (𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑))) | 
| 26 | 25 | adantr 480 | . . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑))) | 
| 27 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑥 ∈ V | 
| 28 |  | limelon 6448 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) | 
| 29 | 27, 28 | mpan 690 | . . . . . . . . . 10
⊢ (Lim
𝑥 → 𝑥 ∈ On) | 
| 30 |  | eloni 6394 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ On → Ord 𝑥) | 
| 31 |  | ordelsuc 7840 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ Ord 𝑥) → (𝐵 ∈ 𝑥 ↔ suc 𝐵 ⊆ 𝑥)) | 
| 32 | 30, 31 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ∈ 𝑥 ↔ suc 𝐵 ⊆ 𝑥)) | 
| 33 |  | onelon 6409 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) | 
| 34 | 33, 14 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦) | 
| 35 | 34, 15 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦 ∈ 𝑥)) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) | 
| 36 | 35 | anassrs 467 | . . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ 𝑥) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) | 
| 37 | 36 | imbi1d 341 | . . . . . . . . . . . . 13
⊢ (((𝐵 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ 𝑥) → ((𝐵 ∈ 𝑦 → 𝜒) ↔ (suc 𝐵 ⊆ 𝑦 → 𝜒))) | 
| 38 | 37 | ralbidva 3176 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) →
(∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) ↔ ∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒))) | 
| 39 | 38 | imbi1d 341 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) →
((∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑) ↔ (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))) | 
| 40 | 32, 39 | imbi12d 344 | . . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ((𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) ↔ (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)))) | 
| 41 | 29, 40 | sylan2 593 | . . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → ((𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) ↔ (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)))) | 
| 42 | 41 | ancoms 458 | . . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → ((𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) ↔ (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)))) | 
| 43 | 26, 42 | mpbid 232 | . . . . . . 7
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))) | 
| 44 | 2, 43 | sylan2br 595 | . . . . . 6
⊢ ((Lim
𝑥 ∧ suc 𝐵 ∈ On) → (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))) | 
| 45 | 44 | imp 406 | . . . . 5
⊢ (((Lim
𝑥 ∧ suc 𝐵 ∈ On) ∧ suc 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)) | 
| 46 | 8, 9, 10, 11, 13, 23, 45 | tfindsg 7882 | . . . 4
⊢ (((𝐴 ∈ On ∧ suc 𝐵 ∈ On) ∧ suc 𝐵 ⊆ 𝐴) → 𝜏) | 
| 47 | 46 | expl 457 | . . 3
⊢ (𝐴 ∈ On → ((suc 𝐵 ∈ On ∧ suc 𝐵 ⊆ 𝐴) → 𝜏)) | 
| 48 | 47 | adantr 480 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → ((suc 𝐵 ∈ On ∧ suc 𝐵 ⊆ 𝐴) → 𝜏)) | 
| 49 | 3, 7, 48 | mp2and 699 | 1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝜏) |