Proof of Theorem isrgrac
Step | Hyp | Ref
| Expression |
1 | | 1st2nd2 7096 |
. 2
⊢ (𝐺 ∈ (𝑋 × 𝑌) → 𝐺 = 〈(1st ‘𝐺), (2nd ‘𝐺)〉) |
2 | | fvex 6113 |
. . . . 5
⊢
(1st ‘𝐺) ∈ V |
3 | 2 | a1i 11 |
. . . 4
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (1st ‘𝐺) ∈ V) |
4 | | fvex 6113 |
. . . . 5
⊢
(2nd ‘𝐺) ∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (2nd ‘𝐺) ∈ V) |
6 | | simpr 476 |
. . . 4
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → 𝐾 ∈ 𝑍) |
7 | | isrgra 26453 |
. . . 4
⊢
(((1st ‘𝐺) ∈ V ∧ (2nd
‘𝐺) ∈ V ∧
𝐾 ∈ 𝑍) → (〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)(((1st ‘𝐺) VDeg (2nd ‘𝐺))‘𝑝) = 𝐾))) |
8 | 3, 5, 6, 7 | syl3anc 1318 |
. . 3
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)(((1st ‘𝐺) VDeg (2nd ‘𝐺))‘𝑝) = 𝐾))) |
9 | | breq1 4586 |
. . . . 5
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
(𝐺 RegGrph 𝐾 ↔ 〈(1st
‘𝐺), (2nd
‘𝐺)〉 RegGrph
𝐾)) |
10 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 → (
VDeg ‘𝐺) = ( VDeg
‘〈(1st ‘𝐺), (2nd ‘𝐺)〉)) |
11 | | df-ov 6552 |
. . . . . . . . . 10
⊢
((1st ‘𝐺) VDeg (2nd ‘𝐺)) = ( VDeg
‘〈(1st ‘𝐺), (2nd ‘𝐺)〉) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 → (
VDeg ‘𝐺) =
((1st ‘𝐺)
VDeg (2nd ‘𝐺))) |
13 | 12 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 → ((
VDeg ‘𝐺)‘𝑝) = (((1st
‘𝐺) VDeg
(2nd ‘𝐺))‘𝑝)) |
14 | 13 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 → (((
VDeg ‘𝐺)‘𝑝) = 𝐾 ↔ (((1st ‘𝐺) VDeg (2nd
‘𝐺))‘𝑝) = 𝐾)) |
15 | 14 | ralbidv 2969 |
. . . . . 6
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
(∀𝑝 ∈
(1st ‘𝐺)((
VDeg ‘𝐺)‘𝑝) = 𝐾 ↔ ∀𝑝 ∈ (1st ‘𝐺)(((1st ‘𝐺) VDeg (2nd
‘𝐺))‘𝑝) = 𝐾)) |
16 | 15 | anbi2d 736 |
. . . . 5
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
((𝐾 ∈
ℕ0 ∧ ∀𝑝 ∈ (1st ‘𝐺)(( VDeg ‘𝐺)‘𝑝) = 𝐾) ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)(((1st ‘𝐺) VDeg (2nd ‘𝐺))‘𝑝) = 𝐾))) |
17 | 9, 16 | bibi12d 334 |
. . . 4
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
((𝐺 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)((
VDeg ‘𝐺)‘𝑝) = 𝐾)) ↔ (〈(1st
‘𝐺), (2nd
‘𝐺)〉 RegGrph
𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)(((1st ‘𝐺) VDeg (2nd ‘𝐺))‘𝑝) = 𝐾)))) |
18 | 17 | adantr 480 |
. . 3
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → ((𝐺 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)((
VDeg ‘𝐺)‘𝑝) = 𝐾)) ↔ (〈(1st
‘𝐺), (2nd
‘𝐺)〉 RegGrph
𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)(((1st ‘𝐺) VDeg (2nd ‘𝐺))‘𝑝) = 𝐾)))) |
19 | 8, 18 | mpbird 246 |
. 2
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)((
VDeg ‘𝐺)‘𝑝) = 𝐾))) |
20 | 1, 19 | sylan 487 |
1
⊢ ((𝐺 ∈ (𝑋 × 𝑌) ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈
(1st ‘𝐺)((
VDeg ‘𝐺)‘𝑝) = 𝐾))) |