Step | Hyp | Ref
| Expression |
1 | | frecabcl.as |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
2 | 1 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = ∅) → 𝐴 ∈ 𝑆) |
3 | | peano1 4576 |
. . . . . . . . 9
⊢ ∅
∈ ω |
4 | | elex2 2746 |
. . . . . . . . 9
⊢ (∅
∈ ω → ∃𝑎 𝑎 ∈ ω) |
5 | | r19.9rmv 3505 |
. . . . . . . . 9
⊢
(∃𝑎 𝑎 ∈ ω → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴)) |
6 | 3, 4, 5 | mp2b 8 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴) |
7 | | frecabcl.g |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝑁⟶𝑆) |
8 | | fdm 5351 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:𝑁⟶𝑆 → dom 𝐺 = 𝑁) |
9 | 7, 8 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐺 = 𝑁) |
10 | 9 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = 𝑁) |
11 | | eqeq2 2180 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = ∅ → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅)) |
12 | 11 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 = ∅) → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅)) |
13 | 10, 12 | mpbid 146 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = ∅) |
14 | 13 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 = ∅) |
15 | 14 | biantrurd 303 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥 ∈ 𝐴 ↔ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) |
16 | | peano3 4578 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ω → suc 𝑚 ≠ ∅) |
17 | 16 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ ∅) |
18 | 17, 14 | neeqtrrd 2370 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ dom 𝐺) |
19 | 18 | necomd 2426 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 ≠ suc 𝑚) |
20 | 19 | neneqd 2361 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ dom 𝐺 = suc 𝑚) |
21 | 20 | intnanrd 927 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) |
22 | | biorf 739 |
. . . . . . . . . . 11
⊢ (¬
(dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
23 | 21, 22 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
24 | 15, 23 | bitrd 187 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥 ∈ 𝐴 ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
25 | 24 | rexbidva 2467 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 = ∅) → (∃𝑚 ∈ ω 𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
26 | 6, 25 | syl5bb 191 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
27 | | r19.44mv 3508 |
. . . . . . . 8
⊢
(∃𝑎 𝑎 ∈ ω →
(∃𝑚 ∈ ω
((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
28 | 3, 4, 27 | mp2b 8 |
. . . . . . 7
⊢
(∃𝑚 ∈
ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) |
29 | 26, 28 | bitrdi 195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
30 | 29 | alrimiv 1867 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = ∅) → ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
31 | 2, 30 | jca 304 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
32 | | eleq1 2233 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (𝑧 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆)) |
33 | | eleq2 2234 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐴)) |
34 | 33 | bibi1d 232 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
35 | 34 | albidv 1817 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
36 | 32, 35 | anbi12d 470 |
. . . . 5
⊢ (𝑧 = 𝐴 → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))) |
37 | 36 | spcegv 2818 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → ((𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))) |
38 | 2, 31, 37 | sylc 62 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = ∅) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
39 | | fveq2 5494 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑘) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑘))) |
40 | 39 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑘) → ((𝐹‘𝑦) ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆)) |
41 | | frecabcl.fs |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆) |
42 | 41 | ad2antrr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆) |
43 | 7 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝐺:𝑁⟶𝑆) |
44 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑘 ∈ V |
45 | 44 | sucid 4400 |
. . . . . . . . . . 11
⊢ 𝑘 ∈ suc 𝑘 |
46 | | eleq2 2234 |
. . . . . . . . . . 11
⊢ (𝑁 = suc 𝑘 → (𝑘 ∈ 𝑁 ↔ 𝑘 ∈ suc 𝑘)) |
47 | 45, 46 | mpbiri 167 |
. . . . . . . . . 10
⊢ (𝑁 = suc 𝑘 → 𝑘 ∈ 𝑁) |
48 | 47 | adantl 275 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ 𝑁) |
49 | 43, 48 | ffvelrnd 5630 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐺‘𝑘) ∈ 𝑆) |
50 | 40, 42, 49 | rspcdva 2839 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐹‘(𝐺‘𝑘)) ∈ 𝑆) |
51 | | simpllr 529 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑘 ∈ ω) |
52 | 43, 8 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 = 𝑁) |
53 | 52 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = 𝑁) |
54 | | simplr 525 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑁 = suc 𝑘) |
55 | 53, 54 | eqtrd 2203 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = suc 𝑘) |
56 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) |
57 | 55, 56 | jca 304 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) |
58 | | suceq 4385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑘 → suc 𝑚 = suc 𝑘) |
59 | 58 | eqeq2d 2182 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑘 → (dom 𝐺 = suc 𝑚 ↔ dom 𝐺 = suc 𝑘)) |
60 | | fveq2 5494 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘)) |
61 | 60 | fveq2d 5498 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑘 → (𝐹‘(𝐺‘𝑚)) = (𝐹‘(𝐺‘𝑘))) |
62 | 61 | eleq2d 2240 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑘 → (𝑥 ∈ (𝐹‘(𝐺‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) |
63 | 59, 62 | anbi12d 470 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑘 → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))) |
64 | 63 | rspcev 2834 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) |
65 | 51, 57, 64 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) |
66 | 65 | ex 114 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))) |
67 | | simpr 109 |
. . . . . . . . . . . . . . 15
⊢ ((dom
𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) |
68 | 67 | adantl 275 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) |
69 | 52 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = 𝑁) |
70 | | simprl 526 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = suc 𝑚) |
71 | | simpllr 529 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑁 = suc 𝑘) |
72 | 69, 70, 71 | 3eqtr3rd 2212 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → suc 𝑘 = suc 𝑚) |
73 | | simplr 525 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ ω) |
74 | 73 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 ∈ ω) |
75 | | simplr 525 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑚 ∈ ω) |
76 | | peano4 4579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ω ∧ 𝑚 ∈ ω) → (suc
𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚)) |
77 | 74, 75, 76 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚)) |
78 | 72, 77 | mpbid 146 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 = 𝑚) |
79 | 78 | fveq2d 5498 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐺‘𝑘) = (𝐺‘𝑚)) |
80 | 79 | fveq2d 5498 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑚))) |
81 | 80 | eleq2d 2240 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) |
82 | 68, 81 | mpbird 166 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) |
83 | 82 | ex 114 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) |
84 | 83 | rexlimdva 2587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) |
85 | 66, 84 | impbid 128 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))) |
86 | 85 | alrimiv 1867 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))) |
87 | | peano3 4578 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ω → suc 𝑘 ≠ ∅) |
88 | 73, 87 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → suc 𝑘 ≠ ∅) |
89 | | neeq1 2353 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = suc 𝑘 → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅)) |
90 | 89 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅)) |
91 | 88, 90 | mpbird 166 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑁 ≠ ∅) |
92 | 52, 91 | eqnetrd 2364 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 ≠ ∅) |
93 | 92 | neneqd 2361 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ dom 𝐺 = ∅) |
94 | 93 | intnanrd 927 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) |
95 | | biorf 739 |
. . . . . . . . . . . . 13
⊢ (¬
(dom 𝐺 = ∅ ∧
𝑥 ∈ 𝐴) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))) |
96 | 94, 95 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))) |
97 | | orcom 723 |
. . . . . . . . . . . 12
⊢ (((dom
𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) |
98 | 96, 97 | bitrdi 195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
99 | 98 | bibi2d 231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
100 | 99 | albidv 1817 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
101 | 86, 100 | mpbid 146 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
102 | 50, 101 | jca 304 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
103 | | eleq1 2233 |
. . . . . . . . 9
⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑧 ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆)) |
104 | | eleq2 2234 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) |
105 | 104 | bibi1d 232 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
106 | 105 | albidv 1817 |
. . . . . . . . 9
⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
107 | 103, 106 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))) |
108 | 107 | spcegv 2818 |
. . . . . . 7
⊢ ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 → (((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))) |
109 | 50, 102, 108 | sylc 62 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
110 | 109 | ex 114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ω) → (𝑁 = suc 𝑘 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))) |
111 | 110 | rexlimdva 2587 |
. . . 4
⊢ (𝜑 → (∃𝑘 ∈ ω 𝑁 = suc 𝑘 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))) |
112 | 111 | imp 123 |
. . 3
⊢ ((𝜑 ∧ ∃𝑘 ∈ ω 𝑁 = suc 𝑘) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
113 | | frecabcl.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ω) |
114 | | nn0suc 4586 |
. . . 4
⊢ (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘)) |
115 | 113, 114 | syl 14 |
. . 3
⊢ (𝜑 → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘)) |
116 | 38, 112, 115 | mpjaodan 793 |
. 2
⊢ (𝜑 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
117 | | clabel 2297 |
. 2
⊢ ({𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆 ↔ ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))) |
118 | 116, 117 | sylibr 133 |
1
⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) |