This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grlimgrtrilem2

Description: Lemma 3 for grlimgrtri . (Contributed by AV, 23-Aug-2025)

Ref Expression
Hypotheses grlimgrtrilem1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
grlimgrtrilem1.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑎 )
grlimgrtrilem1.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
grlimgrtrilem1.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
grlimgrtrilem2.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑎 ) )
grlimgrtrilem2.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
grlimgrtrilem2.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion grlimgrtrilem2 ( ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) ∧ { 𝑏 , 𝑐 } ∈ 𝐾 ) → { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 grlimgrtrilem1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grlimgrtrilem1.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑎 )
3 grlimgrtrilem1.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
4 grlimgrtrilem1.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
5 grlimgrtrilem2.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑎 ) )
6 grlimgrtrilem2.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
7 grlimgrtrilem2.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
8 imaeq2 ⊢ ( 𝑖 = { 𝑏 , 𝑐 } → ( 𝑓 “ 𝑖 ) = ( 𝑓 “ { 𝑏 , 𝑐 } ) )
9 fveq2 ⊢ ( 𝑖 = { 𝑏 , 𝑐 } → ( 𝑔 ‘ 𝑖 ) = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) )
10 8 9 eqeq12d ⊢ ( 𝑖 = { 𝑏 , 𝑐 } → ( ( 𝑓 “ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) ↔ ( 𝑓 “ { 𝑏 , 𝑐 } ) = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) ) )
11 10 rspcv ⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 → ( ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) → ( 𝑓 “ { 𝑏 , 𝑐 } ) = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) ) )
12 f1ofn ⊢ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 → 𝑓 Fn 𝑁 )
13 12 adantr ⊢ ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → 𝑓 Fn 𝑁 )
14 13 adantl ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → 𝑓 Fn 𝑁 )
15 4 eleq2i ⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 ↔ { 𝑏 , 𝑐 } ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } )
16 sseq1 ⊢ ( 𝑥 = { 𝑏 , 𝑐 } → ( 𝑥 ⊆ 𝑁 ↔ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
17 16 elrab ⊢ ( { 𝑏 , 𝑐 } ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } ↔ ( { 𝑏 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
18 15 17 bitri ⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 ↔ ( { 𝑏 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
19 vex ⊢ 𝑏 ∈ V
20 vex ⊢ 𝑐 ∈ V
21 19 20 prss ⊢ ( ( 𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) ↔ { 𝑏 , 𝑐 } ⊆ 𝑁 )
22 simpl ⊢ ( ( 𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
23 21 22 sylbir ⊢ ( { 𝑏 , 𝑐 } ⊆ 𝑁 → 𝑏 ∈ 𝑁 )
24 18 23 simplbiim ⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 → 𝑏 ∈ 𝑁 )
25 24 adantr ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → 𝑏 ∈ 𝑁 )
26 simpr ⊢ ( ( 𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
27 21 26 sylbir ⊢ ( { 𝑏 , 𝑐 } ⊆ 𝑁 → 𝑐 ∈ 𝑁 )
28 18 27 simplbiim ⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 → 𝑐 ∈ 𝑁 )
29 28 adantr ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → 𝑐 ∈ 𝑁 )
30 fnimapr ⊢ ( ( 𝑓 Fn 𝑁 ∧ 𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → ( 𝑓 “ { 𝑏 , 𝑐 } ) = { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } )
31 14 25 29 30 syl3anc ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → ( 𝑓 “ { 𝑏 , 𝑐 } ) = { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } )
32 31 eqeq1d ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → ( ( 𝑓 “ { 𝑏 , 𝑐 } ) = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) ↔ { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) ) )
33 ssrab2 ⊢ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 } ⊆ 𝐽
34 7 33 eqsstri ⊢ 𝐿 ⊆ 𝐽
35 f1of ⊢ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 → 𝑔 : 𝐾 ⟶ 𝐿 )
36 35 adantl ⊢ ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → 𝑔 : 𝐾 ⟶ 𝐿 )
37 36 adantl ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → 𝑔 : 𝐾 ⟶ 𝐿 )
38 simpl ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → { 𝑏 , 𝑐 } ∈ 𝐾 )
39 37 38 ffvelcdmd ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → ( 𝑔 ‘ { 𝑏 , 𝑐 } ) ∈ 𝐿 )
40 34 39 sselid ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → ( 𝑔 ‘ { 𝑏 , 𝑐 } ) ∈ 𝐽 )
41 eleq1 ⊢ ( { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) → ( { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } ∈ 𝐽 ↔ ( 𝑔 ‘ { 𝑏 , 𝑐 } ) ∈ 𝐽 ) )
42 40 41 syl5ibrcom ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → ( { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) → { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } ∈ 𝐽 ) )
43 32 42 sylbid ⊢ ( ( { 𝑏 , 𝑐 } ∈ 𝐾 ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ) → ( ( 𝑓 “ { 𝑏 , 𝑐 } ) = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) → { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } ∈ 𝐽 ) )
44 43 ex ⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 → ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → ( ( 𝑓 “ { 𝑏 , 𝑐 } ) = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) → { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } ∈ 𝐽 ) ) )
45 44 com23 ⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 → ( ( 𝑓 “ { 𝑏 , 𝑐 } ) = ( 𝑔 ‘ { 𝑏 , 𝑐 } ) → ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } ∈ 𝐽 ) ) )
46 11 45 syld ⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 → ( ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) → ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } ∈ 𝐽 ) ) )
47 46 3imp31 ⊢ ( ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) ∧ { 𝑏 , 𝑐 } ∈ 𝐾 ) → { ( 𝑓 ‘ 𝑏 ) , ( 𝑓 ‘ 𝑐 ) } ∈ 𝐽 )