Metamath Proof Explorer

Theorem grlimgrtrilem2

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

Ref Expression
Hypotheses grlimgrtrilem1.v ⊢ V = Vtx ⁡ G
grlimgrtrilem1.n ⊢ N = G ClNeighbVtx a
grlimgrtrilem1.i ⊢ I = Edg ⁡ G
grlimgrtrilem1.k ⊢ K = x ∈ I | x ⊆ N
grlimgrtrilem2.m ⊢ M = H ClNeighbVtx F ⁡ a
grlimgrtrilem2.j ⊢ J = Edg ⁡ H
grlimgrtrilem2.l ⊢ L = x ∈ J | x ⊆ M
Assertion grlimgrtrilem2 ⊢ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f i = g ⁡ i ∧ b c ∈ K → f ⁡ b f ⁡ c ∈ J

Proof

Step Hyp Ref Expression
1 grlimgrtrilem1.v ⊢ V = Vtx ⁡ G
2 grlimgrtrilem1.n ⊢ N = G ClNeighbVtx a
3 grlimgrtrilem1.i ⊢ I = Edg ⁡ G
4 grlimgrtrilem1.k ⊢ K = x ∈ I | x ⊆ N
5 grlimgrtrilem2.m ⊢ M = H ClNeighbVtx F ⁡ a
6 grlimgrtrilem2.j ⊢ J = Edg ⁡ H
7 grlimgrtrilem2.l ⊢ L = x ∈ J | x ⊆ M
8 imaeq2 ⊢ i = b c → f i = f b c
9 fveq2 ⊢ i = b c → g ⁡ i = g ⁡ b c
10 8 9 eqeq12d ⊢ i = b c → f i = g ⁡ i ↔ f b c = g ⁡ b c
11 10 rspcv ⊢ b c ∈ K → ∀ i ∈ K f i = g ⁡ i → f b c = g ⁡ b c
12 f1ofn ⊢ f : N ⟶ 1-1 onto M → f Fn N
13 12 adantr ⊢ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f Fn N
14 13 adantl ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f Fn N
15 4 eleq2i ⊢ b c ∈ K ↔ b c ∈ x ∈ I | x ⊆ N
16 sseq1 ⊢ x = b c → x ⊆ N ↔ b c ⊆ N
17 16 elrab ⊢ b c ∈ x ∈ I | x ⊆ N ↔ b c ∈ I ∧ b c ⊆ N
18 15 17 bitri ⊢ b c ∈ K ↔ b c ∈ I ∧ b c ⊆ N
19 vex ⊢ b ∈ V
20 vex ⊢ c ∈ V
21 19 20 prss ⊢ b ∈ N ∧ c ∈ N ↔ b c ⊆ N
22 simpl ⊢ b ∈ N ∧ c ∈ N → b ∈ N
23 21 22 sylbir ⊢ b c ⊆ N → b ∈ N
24 18 23 simplbiim ⊢ b c ∈ K → b ∈ N
25 24 adantr ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → b ∈ N
26 simpr ⊢ b ∈ N ∧ c ∈ N → c ∈ N
27 21 26 sylbir ⊢ b c ⊆ N → c ∈ N
28 18 27 simplbiim ⊢ b c ∈ K → c ∈ N
29 28 adantr ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → c ∈ N
30 fnimapr ⊢ f Fn N ∧ b ∈ N ∧ c ∈ N → f b c = f ⁡ b f ⁡ c
31 14 25 29 30 syl3anc ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f b c = f ⁡ b f ⁡ c
32 31 eqeq1d ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f b c = g ⁡ b c ↔ f ⁡ b f ⁡ c = g ⁡ b c
33 ssrab2 ⊢ x ∈ J | x ⊆ M ⊆ J
34 7 33 eqsstri ⊢ L ⊆ J
35 f1of ⊢ g : K ⟶ 1-1 onto L → g : K ⟶ L
36 35 adantl ⊢ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → g : K ⟶ L
37 36 adantl ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → g : K ⟶ L
38 simpl ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → b c ∈ K
39 37 38 ffvelcdmd ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → g ⁡ b c ∈ L
40 34 39 sselid ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → g ⁡ b c ∈ J
41 eleq1 ⊢ f ⁡ b f ⁡ c = g ⁡ b c → f ⁡ b f ⁡ c ∈ J ↔ g ⁡ b c ∈ J
42 40 41 syl5ibrcom ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f ⁡ b f ⁡ c = g ⁡ b c → f ⁡ b f ⁡ c ∈ J
43 32 42 sylbid ⊢ b c ∈ K ∧ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f b c = g ⁡ b c → f ⁡ b f ⁡ c ∈ J
44 43 ex ⊢ b c ∈ K → f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f b c = g ⁡ b c → f ⁡ b f ⁡ c ∈ J
45 44 com23 ⊢ b c ∈ K → f b c = g ⁡ b c → f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f ⁡ b f ⁡ c ∈ J
46 11 45 syld ⊢ b c ∈ K → ∀ i ∈ K f i = g ⁡ i → f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L → f ⁡ b f ⁡ c ∈ J
47 46 3imp31 ⊢ f : N ⟶ 1-1 onto M ∧ g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f i = g ⁡ i ∧ b c ∈ K → f ⁡ b f ⁡ c ∈ J