Step | Hyp | Ref
| Expression |
1 | | 0ex 4130 |
. . . . 5
⊢ ∅
∈ V |
2 | | opexg 4228 |
. . . . 5
⊢ ((∅
∈ V ∧ (𝐺‘∅) ∈ 𝑉) → ⟨∅, (𝐺‘∅)⟩ ∈
V) |
3 | 1, 2 | mpan 424 |
. . . 4
⊢ ((𝐺‘∅) ∈ 𝑉 → ⟨∅, (𝐺‘∅)⟩ ∈
V) |
4 | | snidg 3621 |
. . . 4
⊢
(⟨∅, (𝐺‘∅)⟩ ∈ V →
⟨∅, (𝐺‘∅)⟩ ∈ {⟨∅,
(𝐺‘∅)⟩}) |
5 | 3, 4 | syl 14 |
. . 3
⊢ ((𝐺‘∅) ∈ 𝑉 → ⟨∅, (𝐺‘∅)⟩ ∈
{⟨∅, (𝐺‘∅)⟩}) |
6 | | fnsng 5263 |
. . . . 5
⊢ ((∅
∈ V ∧ (𝐺‘∅) ∈ 𝑉) → {⟨∅, (𝐺‘∅)⟩} Fn
{∅}) |
7 | 1, 6 | mpan 424 |
. . . 4
⊢ ((𝐺‘∅) ∈ 𝑉 → {⟨∅, (𝐺‘∅)⟩} Fn
{∅}) |
8 | | fvsng 5712 |
. . . . . . 7
⊢ ((∅
∈ V ∧ (𝐺‘∅) ∈ 𝑉) → ({⟨∅, (𝐺‘∅)⟩}‘∅) =
(𝐺‘∅)) |
9 | 1, 8 | mpan 424 |
. . . . . 6
⊢ ((𝐺‘∅) ∈ 𝑉 → ({⟨∅, (𝐺‘∅)⟩}‘∅) =
(𝐺‘∅)) |
10 | | res0 4911 |
. . . . . . 7
⊢
({⟨∅, (𝐺‘∅)⟩} ↾ ∅) =
∅ |
11 | 10 | fveq2i 5518 |
. . . . . 6
⊢ (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾
∅)) = (𝐺‘∅) |
12 | 9, 11 | eqtr4di 2228 |
. . . . 5
⊢ ((𝐺‘∅) ∈ 𝑉 → ({⟨∅, (𝐺‘∅)⟩}‘∅) =
(𝐺‘({⟨∅,
(𝐺‘∅)⟩}
↾ ∅))) |
13 | | fveq2 5515 |
. . . . . . 7
⊢ (𝑦 = ∅ →
({⟨∅, (𝐺‘∅)⟩}‘𝑦) = ({⟨∅, (𝐺‘∅)⟩}‘∅)) |
14 | | reseq2 4902 |
. . . . . . . 8
⊢ (𝑦 = ∅ →
({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦) = ({⟨∅, (𝐺‘∅)⟩} ↾
∅)) |
15 | 14 | fveq2d 5519 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾
𝑦)) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾
∅))) |
16 | 13, 15 | eqeq12d 2192 |
. . . . . 6
⊢ (𝑦 = ∅ →
(({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)) ↔ ({⟨∅,
(𝐺‘∅)⟩}‘∅) =
(𝐺‘({⟨∅,
(𝐺‘∅)⟩}
↾ ∅)))) |
17 | 1, 16 | ralsn 3635 |
. . . . 5
⊢
(∀𝑦 ∈
{∅} ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)) ↔ ({⟨∅,
(𝐺‘∅)⟩}‘∅) =
(𝐺‘({⟨∅,
(𝐺‘∅)⟩}
↾ ∅))) |
18 | 12, 17 | sylibr 134 |
. . . 4
⊢ ((𝐺‘∅) ∈ 𝑉 → ∀𝑦 ∈ {∅}
({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦))) |
19 | | suc0 4411 |
. . . . . 6
⊢ suc
∅ = {∅} |
20 | | 0elon 4392 |
. . . . . . 7
⊢ ∅
∈ On |
21 | 20 | onsuci 4515 |
. . . . . 6
⊢ suc
∅ ∈ On |
22 | 19, 21 | eqeltrri 2251 |
. . . . 5
⊢ {∅}
∈ On |
23 | | fneq2 5305 |
. . . . . . 7
⊢ (𝑥 = {∅} →
({⟨∅, (𝐺‘∅)⟩} Fn 𝑥 ↔ {⟨∅, (𝐺‘∅)⟩} Fn
{∅})) |
24 | | raleq 2672 |
. . . . . . 7
⊢ (𝑥 = {∅} →
(∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)) ↔ ∀𝑦 ∈ {∅}
({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) |
25 | 23, 24 | anbi12d 473 |
. . . . . 6
⊢ (𝑥 = {∅} →
(({⟨∅, (𝐺‘∅)⟩} Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦))) ↔ ({⟨∅,
(𝐺‘∅)⟩} Fn
{∅} ∧ ∀𝑦
∈ {∅} ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦))))) |
26 | 25 | rspcev 2841 |
. . . . 5
⊢
(({∅} ∈ On ∧ ({⟨∅, (𝐺‘∅)⟩} Fn {∅} ∧
∀𝑦 ∈ {∅}
({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) → ∃𝑥 ∈ On ({⟨∅,
(𝐺‘∅)⟩} Fn
𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) |
27 | 22, 26 | mpan 424 |
. . . 4
⊢
(({⟨∅, (𝐺‘∅)⟩} Fn {∅} ∧
∀𝑦 ∈ {∅}
({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦))) → ∃𝑥 ∈ On ({⟨∅,
(𝐺‘∅)⟩} Fn
𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) |
28 | 7, 18, 27 | syl2anc 411 |
. . 3
⊢ ((𝐺‘∅) ∈ 𝑉 → ∃𝑥 ∈ On ({⟨∅,
(𝐺‘∅)⟩} Fn
𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) |
29 | | snexg 4184 |
. . . . 5
⊢
(⟨∅, (𝐺‘∅)⟩ ∈ V →
{⟨∅, (𝐺‘∅)⟩} ∈
V) |
30 | | eleq2 2241 |
. . . . . . 7
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
(⟨∅, (𝐺‘∅)⟩ ∈ 𝑓 ↔ ⟨∅, (𝐺‘∅)⟩ ∈
{⟨∅, (𝐺‘∅)⟩})) |
31 | | fneq1 5304 |
. . . . . . . . 9
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
(𝑓 Fn 𝑥 ↔ {⟨∅, (𝐺‘∅)⟩} Fn 𝑥)) |
32 | | fveq1 5514 |
. . . . . . . . . . 11
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
(𝑓‘𝑦) = ({⟨∅, (𝐺‘∅)⟩}‘𝑦)) |
33 | | reseq1 4901 |
. . . . . . . . . . . 12
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
(𝑓 ↾ 𝑦) = ({⟨∅, (𝐺‘∅)⟩} ↾
𝑦)) |
34 | 33 | fveq2d 5519 |
. . . . . . . . . . 11
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
(𝐺‘(𝑓 ↾ 𝑦)) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦))) |
35 | 32, 34 | eqeq12d 2192 |
. . . . . . . . . 10
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
((𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) |
36 | 35 | ralbidv 2477 |
. . . . . . . . 9
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
(∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) |
37 | 31, 36 | anbi12d 473 |
. . . . . . . 8
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ({⟨∅, (𝐺‘∅)⟩} Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦))))) |
38 | 37 | rexbidv 2478 |
. . . . . . 7
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
(∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ On ({⟨∅, (𝐺‘∅)⟩} Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦))))) |
39 | 30, 38 | anbi12d 473 |
. . . . . 6
⊢ (𝑓 = {⟨∅, (𝐺‘∅)⟩} →
((⟨∅, (𝐺‘∅)⟩ ∈ 𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))) ↔ (⟨∅, (𝐺‘∅)⟩ ∈
{⟨∅, (𝐺‘∅)⟩} ∧ ∃𝑥 ∈ On ({⟨∅,
(𝐺‘∅)⟩} Fn
𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))))) |
40 | 39 | spcegv 2825 |
. . . . 5
⊢
({⟨∅, (𝐺‘∅)⟩} ∈ V →
((⟨∅, (𝐺‘∅)⟩ ∈ {⟨∅,
(𝐺‘∅)⟩}
∧ ∃𝑥 ∈ On
({⟨∅, (𝐺‘∅)⟩} Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) → ∃𝑓(⟨∅, (𝐺‘∅)⟩ ∈
𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))))) |
41 | 3, 29, 40 | 3syl 17 |
. . . 4
⊢ ((𝐺‘∅) ∈ 𝑉 → ((⟨∅, (𝐺‘∅)⟩ ∈
{⟨∅, (𝐺‘∅)⟩} ∧ ∃𝑥 ∈ On ({⟨∅,
(𝐺‘∅)⟩} Fn
𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) → ∃𝑓(⟨∅, (𝐺‘∅)⟩ ∈
𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))))) |
42 | | tfr.1 |
. . . . . 6
⊢ 𝐹 = recs(𝐺) |
43 | 42 | eleq2i 2244 |
. . . . 5
⊢
(⟨∅, (𝐺‘∅)⟩ ∈ 𝐹 ↔ ⟨∅, (𝐺‘∅)⟩ ∈
recs(𝐺)) |
44 | | df-recs 6305 |
. . . . . 6
⊢
recs(𝐺) = ∪ {𝑓
∣ ∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} |
45 | 44 | eleq2i 2244 |
. . . . 5
⊢
(⟨∅, (𝐺‘∅)⟩ ∈ recs(𝐺) ↔ ⟨∅, (𝐺‘∅)⟩ ∈
∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}) |
46 | | eluniab 3821 |
. . . . 5
⊢
(⟨∅, (𝐺‘∅)⟩ ∈ ∪ {𝑓
∣ ∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} ↔ ∃𝑓(⟨∅, (𝐺‘∅)⟩ ∈ 𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))))) |
47 | 43, 45, 46 | 3bitri 206 |
. . . 4
⊢
(⟨∅, (𝐺‘∅)⟩ ∈ 𝐹 ↔ ∃𝑓(⟨∅, (𝐺‘∅)⟩ ∈
𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))))) |
48 | 41, 47 | imbitrrdi 162 |
. . 3
⊢ ((𝐺‘∅) ∈ 𝑉 → ((⟨∅, (𝐺‘∅)⟩ ∈
{⟨∅, (𝐺‘∅)⟩} ∧ ∃𝑥 ∈ On ({⟨∅,
(𝐺‘∅)⟩} Fn
𝑥 ∧ ∀𝑦 ∈ 𝑥 ({⟨∅, (𝐺‘∅)⟩}‘𝑦) = (𝐺‘({⟨∅, (𝐺‘∅)⟩} ↾ 𝑦)))) → ⟨∅,
(𝐺‘∅)⟩
∈ 𝐹)) |
49 | 5, 28, 48 | mp2and 433 |
. 2
⊢ ((𝐺‘∅) ∈ 𝑉 → ⟨∅, (𝐺‘∅)⟩ ∈
𝐹) |
50 | | opeldmg 4832 |
. . 3
⊢ ((∅
∈ V ∧ (𝐺‘∅) ∈ 𝑉) → (⟨∅, (𝐺‘∅)⟩ ∈ 𝐹 → ∅ ∈ dom 𝐹)) |
51 | 1, 50 | mpan 424 |
. 2
⊢ ((𝐺‘∅) ∈ 𝑉 → (⟨∅, (𝐺‘∅)⟩ ∈
𝐹 → ∅ ∈ dom
𝐹)) |
52 | 49, 51 | mpd 13 |
1
⊢ ((𝐺‘∅) ∈ 𝑉 → ∅ ∈ dom 𝐹) |