Step | Hyp | Ref
| Expression |
1 | | 0lt2o 6470 |
. . . 4
⊢ ∅
∈ 2o |
2 | | funfvex 5554 |
. . . . 5
⊢ ((Fun
𝐺 ∧ ∅ ∈ dom
𝐺) → (𝐺‘∅) ∈
V) |
3 | 2 | funfni 5338 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ ∅
∈ 2o) → (𝐺‘∅) ∈ V) |
4 | 1, 3 | mpan2 425 |
. . 3
⊢ (𝐺 Fn 2o → (𝐺‘∅) ∈
V) |
5 | | 1lt2o 6471 |
. . . 4
⊢
1o ∈ 2o |
6 | | funfvex 5554 |
. . . . 5
⊢ ((Fun
𝐺 ∧ 1o
∈ dom 𝐺) → (𝐺‘1o) ∈
V) |
7 | 6 | funfni 5338 |
. . . 4
⊢ ((𝐺 Fn 2o ∧
1o ∈ 2o) → (𝐺‘1o) ∈
V) |
8 | 5, 7 | mpan2 425 |
. . 3
⊢ (𝐺 Fn 2o → (𝐺‘1o) ∈
V) |
9 | | fnpr2o 12827 |
. . 3
⊢ (((𝐺‘∅) ∈ V ∧
(𝐺‘1o)
∈ V) → {⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩} Fn
2o) |
10 | 4, 8, 9 | syl2anc 411 |
. 2
⊢ (𝐺 Fn 2o →
{⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩} Fn
2o) |
11 | | id 19 |
. 2
⊢ (𝐺 Fn 2o → 𝐺 Fn
2o) |
12 | | elpri 3633 |
. . . 4
⊢ (𝑘 ∈ {∅, 1o}
→ (𝑘 = ∅ ∨
𝑘 =
1o)) |
13 | | df2o3 6459 |
. . . 4
⊢
2o = {∅, 1o} |
14 | 12, 13 | eleq2s 2284 |
. . 3
⊢ (𝑘 ∈ 2o →
(𝑘 = ∅ ∨ 𝑘 =
1o)) |
15 | | fvpr0o 12829 |
. . . . . . 7
⊢ ((𝐺‘∅) ∈ V →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘∅)
= (𝐺‘∅)) |
16 | 4, 15 | syl 14 |
. . . . . 6
⊢ (𝐺 Fn 2o →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘∅)
= (𝐺‘∅)) |
17 | 16 | adantr 276 |
. . . . 5
⊢ ((𝐺 Fn 2o ∧ 𝑘 = ∅) →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘∅)
= (𝐺‘∅)) |
18 | | fveq2 5537 |
. . . . . 6
⊢ (𝑘 = ∅ →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘𝑘) = ({⟨∅, (𝐺‘∅)⟩,
⟨1o, (𝐺‘1o)⟩}‘∅)) |
19 | 18 | adantl 277 |
. . . . 5
⊢ ((𝐺 Fn 2o ∧ 𝑘 = ∅) →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘𝑘) = ({⟨∅, (𝐺‘∅)⟩,
⟨1o, (𝐺‘1o)⟩}‘∅)) |
20 | | fveq2 5537 |
. . . . . 6
⊢ (𝑘 = ∅ → (𝐺‘𝑘) = (𝐺‘∅)) |
21 | 20 | adantl 277 |
. . . . 5
⊢ ((𝐺 Fn 2o ∧ 𝑘 = ∅) → (𝐺‘𝑘) = (𝐺‘∅)) |
22 | 17, 19, 21 | 3eqtr4d 2232 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ 𝑘 = ∅) →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘𝑘) = (𝐺‘𝑘)) |
23 | | fvpr1o 12830 |
. . . . . . 7
⊢ ((𝐺‘1o) ∈ V
→ ({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘1o)
= (𝐺‘1o)) |
24 | 8, 23 | syl 14 |
. . . . . 6
⊢ (𝐺 Fn 2o →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘1o)
= (𝐺‘1o)) |
25 | 24 | adantr 276 |
. . . . 5
⊢ ((𝐺 Fn 2o ∧ 𝑘 = 1o) →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘1o)
= (𝐺‘1o)) |
26 | | fveq2 5537 |
. . . . . 6
⊢ (𝑘 = 1o →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘𝑘) = ({⟨∅, (𝐺‘∅)⟩,
⟨1o, (𝐺‘1o)⟩}‘1o)) |
27 | 26 | adantl 277 |
. . . . 5
⊢ ((𝐺 Fn 2o ∧ 𝑘 = 1o) →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘𝑘) = ({⟨∅, (𝐺‘∅)⟩,
⟨1o, (𝐺‘1o)⟩}‘1o)) |
28 | | fveq2 5537 |
. . . . . 6
⊢ (𝑘 = 1o → (𝐺‘𝑘) = (𝐺‘1o)) |
29 | 28 | adantl 277 |
. . . . 5
⊢ ((𝐺 Fn 2o ∧ 𝑘 = 1o) → (𝐺‘𝑘) = (𝐺‘1o)) |
30 | 25, 27, 29 | 3eqtr4d 2232 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ 𝑘 = 1o) →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘𝑘) = (𝐺‘𝑘)) |
31 | 22, 30 | jaodan 798 |
. . 3
⊢ ((𝐺 Fn 2o ∧ (𝑘 = ∅ ∨ 𝑘 = 1o)) →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘𝑘) = (𝐺‘𝑘)) |
32 | 14, 31 | sylan2 286 |
. 2
⊢ ((𝐺 Fn 2o ∧ 𝑘 ∈ 2o) →
({⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩}‘𝑘) = (𝐺‘𝑘)) |
33 | 10, 11, 32 | eqfnfvd 5640 |
1
⊢ (𝐺 Fn 2o →
{⟨∅, (𝐺‘∅)⟩, ⟨1o,
(𝐺‘1o)⟩} = 𝐺) |