Proof of Theorem tfindsg
Step | Hyp | Ref
| Expression |
1 | | sseq2 3948 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅)) |
2 | 1 | adantl 482 |
. . . . . 6
⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅)) |
3 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (𝑥 = 𝐵 ↔ 𝑥 = ∅)) |
4 | | tfindsg.1 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) |
5 | 3, 4 | syl6bir 253 |
. . . . . . 7
⊢ (𝐵 = ∅ → (𝑥 = ∅ → (𝜑 ↔ 𝜓))) |
6 | 5 | imp 407 |
. . . . . 6
⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑 ↔ 𝜓)) |
7 | 2, 6 | imbi12d 345 |
. . . . 5
⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) |
8 | 1 | imbi1d 342 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑))) |
9 | | ss0 4334 |
. . . . . . . . 9
⊢ (𝐵 ⊆ ∅ → 𝐵 = ∅) |
10 | 9 | con3i 154 |
. . . . . . . 8
⊢ (¬
𝐵 = ∅ → ¬
𝐵 ⊆
∅) |
11 | 10 | pm2.21d 121 |
. . . . . . 7
⊢ (¬
𝐵 = ∅ → (𝐵 ⊆ ∅ → (𝜑 ↔ 𝜓))) |
12 | 11 | pm5.74d 272 |
. . . . . 6
⊢ (¬
𝐵 = ∅ → ((𝐵 ⊆ ∅ → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) |
13 | 8, 12 | sylan9bbr 511 |
. . . . 5
⊢ ((¬
𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) |
14 | 7, 13 | pm2.61ian 809 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓))) |
15 | 14 | imbi2d 341 |
. . 3
⊢ (𝑥 = ∅ → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓)))) |
16 | | sseq2 3948 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦)) |
17 | | tfindsg.2 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
18 | 16, 17 | imbi12d 345 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝑦 → 𝜒))) |
19 | 18 | imbi2d 341 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)))) |
20 | | sseq2 3948 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ suc 𝑦)) |
21 | | tfindsg.3 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) |
22 | 20, 21 | imbi12d 345 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ suc 𝑦 → 𝜃))) |
23 | 22 | imbi2d 341 |
. . 3
⊢ (𝑥 = suc 𝑦 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
24 | | sseq2 3948 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝐴)) |
25 | | tfindsg.4 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
26 | 24, 25 | imbi12d 345 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝐴 → 𝜏))) |
27 | 26 | imbi2d 341 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ 𝐴 → 𝜏)))) |
28 | | tfindsg.5 |
. . . 4
⊢ (𝐵 ∈ On → 𝜓) |
29 | 28 | a1d 25 |
. . 3
⊢ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓)) |
30 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
31 | 30 | sucex 7656 |
. . . . . . . . . . . . 13
⊢ suc 𝑦 ∈ V |
32 | 31 | eqvinc 3580 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵)) |
33 | 28, 4 | syl5ibr 245 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → (𝐵 ∈ On → 𝜑)) |
34 | 21 | biimpd 228 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝑦 → (𝜑 → 𝜃)) |
35 | 33, 34 | sylan9r 509 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃)) |
36 | 35 | exlimiv 1933 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃)) |
37 | 32, 36 | sylbi 216 |
. . . . . . . . . . 11
⊢ (suc
𝑦 = 𝐵 → (𝐵 ∈ On → 𝜃)) |
38 | 37 | eqcoms 2746 |
. . . . . . . . . 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 482 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
43 | | df-ne 2944 |
. . . . . . . . 9
⊢ (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦) |
44 | 43 | anbi2i 623 |
. . . . . . . 8
⊢ ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) ↔ (𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦)) |
45 | | annim 404 |
. . . . . . . 8
⊢ ((𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦)) |
46 | 44, 45 | bitri 274 |
. . . . . . 7
⊢ ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦)) |
47 | | onsssuc 6355 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ 𝐵 ∈ suc 𝑦)) |
48 | | suceloni 7659 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
49 | | onelpss 6308 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) |
50 | 48, 49 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) |
51 | 47, 50 | bitrd 278 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) |
52 | 51 | ancoms 459 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦))) |
53 | | tfindsg.6 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) |
54 | 53 | ex 413 |
. . . . . . . . . . 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 259 |
. . . . . . 7
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
59 | 46, 58 | syl5bir 242 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
60 | 42, 59 | pm2.61d 179 |
. . . . 5
⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))) |
61 | 60 | ex 413 |
. . . 4
⊢ (𝑦 ∈ On → (𝐵 ∈ On → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
62 | 61 | a2d 29 |
. . 3
⊢ (𝑦 ∈ On → ((𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦 → 𝜃)))) |
63 | | pm2.27 42 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → ((𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ⊆ 𝑦 → 𝜒))) |
64 | 63 | ralimdv 3109 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → ∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒))) |
65 | 64 | ad2antlr 724 |
. . . . . . 7
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → ∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒))) |
66 | | tfindsg.7 |
. . . . . . 7
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)) |
67 | 65, 66 | syld 47 |
. . . . . 6
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → 𝜑)) |
68 | 67 | exp31 420 |
. . . . 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 7706 |
. 2
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐵 ⊆ 𝐴 → 𝜏))) |
72 | 71 | imp31 418 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → 𝜏) |