Proof of Theorem isrusgusrgcl
Step | Hyp | Ref
| Expression |
1 | | 1st2nd2 7096 |
. 2
⊢ (𝐺 ∈ (𝑋 × 𝑌) → 𝐺 = 〈(1st ‘𝐺), (2nd ‘𝐺)〉) |
2 | | breq1 4586 |
. . . 4
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
(𝐺 RegUSGrph 𝐾 ↔ 〈(1st
‘𝐺), (2nd
‘𝐺)〉 RegUSGrph
𝐾)) |
3 | 2 | adantr 480 |
. . 3
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGrph 𝐾 ↔ 〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegUSGrph 𝐾)) |
4 | | fvex 6113 |
. . . . 5
⊢
(1st ‘𝐺) ∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (1st ‘𝐺) ∈ V) |
6 | | fvex 6113 |
. . . . 5
⊢
(2nd ‘𝐺) ∈ V |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (2nd ‘𝐺) ∈ V) |
8 | | simpr 476 |
. . . 4
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → 𝐾 ∈ 𝑍) |
9 | | isrusgusrg 26459 |
. . . 4
⊢
(((1st ‘𝐺) ∈ V ∧ (2nd
‘𝐺) ∈ V ∧
𝐾 ∈ 𝑍) → (〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegUSGrph 𝐾 ↔ ((1st
‘𝐺) USGrph
(2nd ‘𝐺)
∧ 〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegGrph 𝐾))) |
10 | 5, 7, 8, 9 | syl3anc 1318 |
. . 3
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegUSGrph 𝐾 ↔ ((1st
‘𝐺) USGrph
(2nd ‘𝐺)
∧ 〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegGrph 𝐾))) |
11 | | eleq1 2676 |
. . . . . . 7
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
(𝐺 ∈ USGrph ↔
〈(1st ‘𝐺), (2nd ‘𝐺)〉 ∈ USGrph )) |
12 | | df-br 4584 |
. . . . . . 7
⊢
((1st ‘𝐺) USGrph (2nd ‘𝐺) ↔ 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∈
USGrph ) |
13 | 11, 12 | syl6bbr 277 |
. . . . . 6
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
(𝐺 ∈ USGrph ↔
(1st ‘𝐺)
USGrph (2nd ‘𝐺))) |
14 | | breq1 4586 |
. . . . . 6
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
(𝐺 RegGrph 𝐾 ↔ 〈(1st
‘𝐺), (2nd
‘𝐺)〉 RegGrph
𝐾)) |
15 | 13, 14 | anbi12d 743 |
. . . . 5
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
((𝐺 ∈ USGrph ∧
𝐺 RegGrph 𝐾) ↔ ((1st ‘𝐺) USGrph (2nd
‘𝐺) ∧
〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegGrph 𝐾))) |
16 | 15 | bicomd 212 |
. . . 4
⊢ (𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 →
(((1st ‘𝐺)
USGrph (2nd ‘𝐺) ∧ 〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegGrph 𝐾) ↔ (𝐺 ∈ USGrph ∧ 𝐺 RegGrph 𝐾))) |
17 | 16 | adantr 480 |
. . 3
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (((1st ‘𝐺) USGrph (2nd
‘𝐺) ∧
〈(1st ‘𝐺), (2nd ‘𝐺)〉 RegGrph 𝐾) ↔ (𝐺 ∈ USGrph ∧ 𝐺 RegGrph 𝐾))) |
18 | 3, 10, 17 | 3bitrd 293 |
. 2
⊢ ((𝐺 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGrph 𝐾 ↔ (𝐺 ∈ USGrph ∧ 𝐺 RegGrph 𝐾))) |
19 | 1, 18 | sylan 487 |
1
⊢ ((𝐺 ∈ (𝑋 × 𝑌) ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGrph 𝐾 ↔ (𝐺 ∈ USGrph ∧ 𝐺 RegGrph 𝐾))) |