Proof of Theorem tfindsg2
Step | Hyp | Ref
| Expression |
1 | | onelon 6238 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
2 | | sucelon 7596 |
. . 3
⊢ (𝐵 ∈ On ↔ suc 𝐵 ∈ On) |
3 | 1, 2 | sylib 221 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → suc 𝐵 ∈ On) |
4 | | eloni 6223 |
. . . 4
⊢ (𝐴 ∈ On → Ord 𝐴) |
5 | | ordsucss 7597 |
. . . 4
⊢ (Ord
𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴)) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴)) |
7 | 6 | imp 410 |
. 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 238 |
. . . . 5
⊢ (suc
𝐵 ∈ On → 𝜓) |
14 | | eloni 6223 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → Ord 𝑦) |
15 | | ordelsuc 7599 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ Ord 𝑦) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) |
16 | 14, 15 | sylan2 596 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) |
17 | 16 | ancoms 462 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) |
18 | | tfindsg2.6 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ 𝑦) → (𝜒 → 𝜃)) |
19 | 18 | ex 416 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (𝐵 ∈ 𝑦 → (𝜒 → 𝜃))) |
20 | 19 | adantr 484 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ∈ 𝑦 → (𝜒 → 𝜃))) |
21 | 17, 20 | sylbird 263 |
. . . . . . 7
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (suc 𝐵 ⊆ 𝑦 → (𝜒 → 𝜃))) |
22 | 2, 21 | sylan2br 598 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ suc 𝐵 ∈ On) → (suc 𝐵 ⊆ 𝑦 → (𝜒 → 𝜃))) |
23 | 22 | imp 410 |
. . . . 5
⊢ (((𝑦 ∈ On ∧ suc 𝐵 ∈ On) ∧ suc 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) |
24 | | tfindsg2.7 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) |
25 | 24 | ex 416 |
. . . . . . . . 9
⊢ (Lim
𝑥 → (𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑))) |
26 | 25 | adantr 484 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑))) |
27 | | vex 3412 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
28 | | limelon 6276 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
29 | 27, 28 | mpan 690 |
. . . . . . . . . 10
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
30 | | eloni 6223 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → Ord 𝑥) |
31 | | ordelsuc 7599 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ Ord 𝑥) → (𝐵 ∈ 𝑥 ↔ suc 𝐵 ⊆ 𝑥)) |
32 | 30, 31 | sylan2 596 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ∈ 𝑥 ↔ suc 𝐵 ⊆ 𝑥)) |
33 | | onelon 6238 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
34 | 33, 14 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦) |
35 | 34, 15 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦 ∈ 𝑥)) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) |
36 | 35 | anassrs 471 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ 𝑥) → (𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦)) |
37 | 36 | imbi1d 345 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ 𝑥) → ((𝐵 ∈ 𝑦 → 𝜒) ↔ (suc 𝐵 ⊆ 𝑦 → 𝜒))) |
38 | 37 | ralbidva 3117 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) →
(∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) ↔ ∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒))) |
39 | 38 | imbi1d 345 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) →
((∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑) ↔ (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))) |
40 | 32, 39 | imbi12d 348 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ((𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) ↔ (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)))) |
41 | 29, 40 | sylan2 596 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → ((𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) ↔ (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)))) |
42 | 41 | ancoms 462 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → ((𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) ↔ (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)))) |
43 | 26, 42 | mpbid 235 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))) |
44 | 2, 43 | sylan2br 598 |
. . . . . 6
⊢ ((Lim
𝑥 ∧ suc 𝐵 ∈ On) → (suc 𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))) |
45 | 44 | imp 410 |
. . . . 5
⊢ (((Lim
𝑥 ∧ suc 𝐵 ∈ On) ∧ suc 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (suc 𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)) |
46 | 8, 9, 10, 11, 13, 23, 45 | tfindsg 7639 |
. . . 4
⊢ (((𝐴 ∈ On ∧ suc 𝐵 ∈ On) ∧ suc 𝐵 ⊆ 𝐴) → 𝜏) |
47 | 46 | expl 461 |
. . 3
⊢ (𝐴 ∈ On → ((suc 𝐵 ∈ On ∧ suc 𝐵 ⊆ 𝐴) → 𝜏)) |
48 | 47 | adantr 484 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → ((suc 𝐵 ∈ On ∧ suc 𝐵 ⊆ 𝐴) → 𝜏)) |
49 | 3, 7, 48 | mp2and 699 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝜏) |