| Step |
Hyp |
Ref |
Expression |
| 1 |
|
grimgrtri.g |
⊢ ( 𝜑 → 𝐺 ∈ UHGraph ) |
| 2 |
|
grimgrtri.h |
⊢ ( 𝜑 → 𝐻 ∈ UHGraph ) |
| 3 |
|
grimgrtri.n |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) |
| 4 |
|
grimgrtri.t |
⊢ ( 𝜑 → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ) |
| 5 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 6 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
| 7 |
5 6
|
grtriprop |
⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
| 8 |
4 7
|
syl |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
| 9 |
|
eqid |
⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 ) |
| 10 |
5 9
|
grimf1o |
⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) |
| 11 |
|
f1of1 |
⊢ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ) |
| 12 |
3 10 11
|
3syl |
⊢ ( 𝜑 → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ) |
| 13 |
12
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ) |
| 14 |
|
simplrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑎 ∈ ( Vtx ‘ 𝐺 ) ) |
| 15 |
14
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → 𝑎 ∈ ( Vtx ‘ 𝐺 ) ) |
| 16 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) |
| 17 |
16
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) |
| 18 |
17
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) |
| 19 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) |
| 20 |
15 18 19
|
3jca |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) |
| 21 |
|
3simpa |
⊢ ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) |
| 22 |
21
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) |
| 23 |
|
grtrimap |
⊢ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) ) ) |
| 24 |
23
|
imp |
⊢ ( ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) ) |
| 25 |
13 20 22 24
|
syl12anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) ) |
| 26 |
|
eqid |
⊢ ( Edg ‘ 𝐻 ) = ( Edg ‘ 𝐻 ) |
| 27 |
5 6 26
|
grimedg |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ) ) |
| 28 |
5 6 26
|
grimedg |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) ) |
| 29 |
5 6 26
|
grimedg |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) ) |
| 30 |
27 28 29
|
3anbi123d |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) ) ) |
| 31 |
|
f1ofn |
⊢ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 Fn ( Vtx ‘ 𝐺 ) ) |
| 32 |
|
simpl |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝐹 Fn ( Vtx ‘ 𝐺 ) ) |
| 33 |
|
simprll |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑎 ∈ ( Vtx ‘ 𝐺 ) ) |
| 34 |
|
simprlr |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) |
| 35 |
|
fnimapr |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐹 “ { 𝑎 , 𝑏 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ) |
| 36 |
32 33 34 35
|
syl3anc |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐹 “ { 𝑎 , 𝑏 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ) |
| 37 |
36
|
eleq1d |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 38 |
37
|
biimpd |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 39 |
38
|
adantrd |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 40 |
|
simprr |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) |
| 41 |
|
fnimapr |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐹 “ { 𝑎 , 𝑐 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ) |
| 42 |
32 33 40 41
|
syl3anc |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐹 “ { 𝑎 , 𝑐 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ) |
| 43 |
42
|
eleq1d |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 44 |
43
|
biimpd |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 45 |
44
|
adantrd |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 46 |
|
fnimapr |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐹 “ { 𝑏 , 𝑐 } ) = { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ) |
| 47 |
32 34 40 46
|
syl3anc |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐹 “ { 𝑏 , 𝑐 } ) = { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ) |
| 48 |
47
|
eleq1d |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 49 |
48
|
biimpd |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) → { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 50 |
49
|
adantrd |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) → { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 51 |
39 45 50
|
3anim123d |
⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 52 |
51
|
ex |
⊢ ( 𝐹 Fn ( Vtx ‘ 𝐺 ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 53 |
52
|
com23 |
⊢ ( 𝐹 Fn ( Vtx ‘ 𝐺 ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 54 |
10 31 53
|
3syl |
⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 55 |
54
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 56 |
30 55
|
sylbid |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 57 |
56
|
2a1d |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } → ( ( ♯ ‘ 𝑇 ) = 3 → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) ) ) |
| 58 |
57
|
3impd |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 59 |
58
|
com23 |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 60 |
1 2 3 59
|
syl3anc |
⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 61 |
60
|
impl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 62 |
61
|
imp |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 63 |
|
tpeq1 |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → { 𝑥 , 𝑦 , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ) |
| 64 |
63
|
eqeq2d |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ↔ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ) ) |
| 65 |
|
preq1 |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → { 𝑥 , 𝑦 } = { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ) |
| 66 |
65
|
eleq1d |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 67 |
|
preq1 |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → { 𝑥 , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ) |
| 68 |
67
|
eleq1d |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 69 |
66 68
|
3anbi12d |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ↔ ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 70 |
64 69
|
3anbi13d |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ↔ ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 71 |
|
tpeq2 |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ) |
| 72 |
71
|
eqeq2d |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ↔ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ) ) |
| 73 |
|
preq2 |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → { ( 𝐹 ‘ 𝑎 ) , 𝑦 } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ) |
| 74 |
73
|
eleq1d |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 75 |
|
preq1 |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → { 𝑦 , 𝑧 } = { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ) |
| 76 |
75
|
eleq1d |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 77 |
74 76
|
3anbi13d |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ↔ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 78 |
72 77
|
3anbi13d |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ↔ ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 79 |
|
tpeq3 |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ) |
| 80 |
79
|
eqeq2d |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ↔ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ) ) |
| 81 |
|
preq2 |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → { ( 𝐹 ‘ 𝑎 ) , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ) |
| 82 |
81
|
eleq1d |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 83 |
|
preq2 |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → { ( 𝐹 ‘ 𝑏 ) , 𝑧 } = { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ) |
| 84 |
83
|
eleq1d |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) |
| 85 |
82 84
|
3anbi23d |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ↔ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 86 |
80 85
|
3anbi13d |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ↔ ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 87 |
70 78 86
|
rspc3ev |
⊢ ( ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 88 |
87
|
3exp2 |
⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) → ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } → ( ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 → ( ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) ) ) |
| 89 |
88
|
3imp |
⊢ ( ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) → ( ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 90 |
25 62 89
|
sylc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 91 |
90
|
rexlimdva2 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 92 |
91
|
rexlimdvva |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) |
| 93 |
8 92
|
mpd |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 94 |
9 26
|
isgrtri |
⊢ ( ( 𝐹 “ 𝑇 ) ∈ ( GrTriangles ‘ 𝐻 ) ↔ ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) |
| 95 |
93 94
|
sylibr |
⊢ ( 𝜑 → ( 𝐹 “ 𝑇 ) ∈ ( GrTriangles ‘ 𝐻 ) ) |