Proof of Theorem tfinds2
Step | Hyp | Ref
| Expression |
1 | | tfinds2.4 |
. . 3
⊢ (𝜏 → 𝜓) |
2 | | 0ex 4790 |
. . . 4
⊢ ∅
∈ V |
3 | | tfinds2.1 |
. . . . 5
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) |
4 | 3 | imbi2d 330 |
. . . 4
⊢ (𝑥 = ∅ → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜓))) |
5 | 2, 4 | sbcie 3470 |
. . 3
⊢
([∅ / 𝑥](𝜏 → 𝜑) ↔ (𝜏 → 𝜓)) |
6 | 1, 5 | mpbir 221 |
. 2
⊢
[∅ / 𝑥](𝜏 → 𝜑) |
7 | | vex 3203 |
. . . . . 6
⊢ 𝑥 ∈ V |
8 | | tfinds2.5 |
. . . . . . . 8
⊢ (𝑦 ∈ On → (𝜏 → (𝜒 → 𝜃))) |
9 | 8 | a2d 29 |
. . . . . . 7
⊢ (𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) |
10 | 9 | sbcth 3450 |
. . . . . 6
⊢ (𝑥 ∈ V → [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃)))) |
11 | 7, 10 | ax-mp 5 |
. . . . 5
⊢
[𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) |
12 | | sbcimg 3477 |
. . . . . 6
⊢ (𝑥 ∈ V → ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃))))) |
13 | 7, 12 | ax-mp 5 |
. . . . 5
⊢
([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)))) |
14 | 11, 13 | mpbi 220 |
. . . 4
⊢
([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃))) |
15 | | sbcel1v 3495 |
. . . 4
⊢
([𝑥 / 𝑦]𝑦 ∈ On ↔ 𝑥 ∈ On) |
16 | | sbcimg 3477 |
. . . . 5
⊢ (𝑥 ∈ V → ([𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)) ↔ ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃)))) |
17 | 7, 16 | ax-mp 5 |
. . . 4
⊢
([𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)) ↔ ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃))) |
18 | 14, 15, 17 | 3imtr3i 280 |
. . 3
⊢ (𝑥 ∈ On → ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃))) |
19 | | tfinds2.2 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
20 | 19 | bicomd 213 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑)) |
21 | 20 | equcoms 1947 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝜒 ↔ 𝜑)) |
22 | 21 | imbi2d 330 |
. . . 4
⊢ (𝑦 = 𝑥 → ((𝜏 → 𝜒) ↔ (𝜏 → 𝜑))) |
23 | 7, 22 | sbcie 3470 |
. . 3
⊢
([𝑥 / 𝑦](𝜏 → 𝜒) ↔ (𝜏 → 𝜑)) |
24 | | vex 3203 |
. . . . . . 7
⊢ 𝑦 ∈ V |
25 | 24 | sucex 7011 |
. . . . . 6
⊢ suc 𝑦 ∈ V |
26 | | tfinds2.3 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) |
27 | 26 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜃))) |
28 | 25, 27 | sbcie 3470 |
. . . . 5
⊢
([suc 𝑦 /
𝑥](𝜏 → 𝜑) ↔ (𝜏 → 𝜃)) |
29 | 28 | sbcbii 3491 |
. . . 4
⊢
([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏 → 𝜑) ↔ [𝑥 / 𝑦](𝜏 → 𝜃)) |
30 | | suceq 5790 |
. . . . 5
⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦) |
31 | 30 | sbcco2 3459 |
. . . 4
⊢
([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏 → 𝜑) ↔ [suc 𝑥 / 𝑥](𝜏 → 𝜑)) |
32 | 29, 31 | bitr3i 266 |
. . 3
⊢
([𝑥 / 𝑦](𝜏 → 𝜃) ↔ [suc 𝑥 / 𝑥](𝜏 → 𝜑)) |
33 | 18, 23, 32 | 3imtr3g 284 |
. 2
⊢ (𝑥 ∈ On → ((𝜏 → 𝜑) → [suc 𝑥 / 𝑥](𝜏 → 𝜑))) |
34 | | sbsbc 3439 |
. . . 4
⊢ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒)) |
35 | 22 | sbralie 3184 |
. . . 4
⊢ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ ∀𝑥 ∈ 𝑦 (𝜏 → 𝜑)) |
36 | 34, 35 | bitr3i 266 |
. . 3
⊢
([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ ∀𝑥 ∈ 𝑦 (𝜏 → 𝜑)) |
37 | | r19.21v 2960 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑥 (𝜏 → 𝜒) ↔ (𝜏 → ∀𝑦 ∈ 𝑥 𝜒)) |
38 | | tfinds2.6 |
. . . . . . . . 9
⊢ (Lim
𝑥 → (𝜏 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) |
39 | 38 | a2d 29 |
. . . . . . . 8
⊢ (Lim
𝑥 → ((𝜏 → ∀𝑦 ∈ 𝑥 𝜒) → (𝜏 → 𝜑))) |
40 | 37, 39 | syl5bi 232 |
. . . . . . 7
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) |
41 | 40 | sbcth 3450 |
. . . . . 6
⊢ (𝑦 ∈ V → [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))) |
42 | 24, 41 | ax-mp 5 |
. . . . 5
⊢
[𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) |
43 | | sbcimg 3477 |
. . . . . 6
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))))) |
44 | 24, 43 | ax-mp 5 |
. . . . 5
⊢
([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))) |
45 | 42, 44 | mpbi 220 |
. . . 4
⊢
([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) |
46 | | limeq 5735 |
. . . . 5
⊢ (𝑥 = 𝑦 → (Lim 𝑥 ↔ Lim 𝑦)) |
47 | 24, 46 | sbcie 3470 |
. . . 4
⊢
([𝑦 / 𝑥]Lim 𝑥 ↔ Lim 𝑦) |
48 | | sbcimg 3477 |
. . . . 5
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)) ↔ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑)))) |
49 | 24, 48 | ax-mp 5 |
. . . 4
⊢
([𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)) ↔ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑))) |
50 | 45, 47, 49 | 3imtr3i 280 |
. . 3
⊢ (Lim
𝑦 → ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑))) |
51 | 36, 50 | syl5bir 233 |
. 2
⊢ (Lim
𝑦 → (∀𝑥 ∈ 𝑦 (𝜏 → 𝜑) → [𝑦 / 𝑥](𝜏 → 𝜑))) |
52 | 6, 33, 51 | tfindes 7062 |
1
⊢ (𝑥 ∈ On → (𝜏 → 𝜑)) |