Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  grlimgrtri Structured version   Visualization version   GIF version
Theorem grlimgrtri 49070
Description: If one of two locally isomorphic graphs has a triangle, so does the other. The triangle in the other graph is not necessarily the image (𝐹 “ 𝑇) of the triangle 𝑇 in the first graph. (Contributed by AV, 24-Aug-2025.)
Hypotheses
Ref Expression
grlimgrtri.g (𝜑 → 𝐺 ∈ USPGraph)
grlimgrtri.h (𝜑 → 𝐻 ∈ USPGraph)
grlimgrtri.n (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
grlimgrtri.t (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺))
Assertion
Ref Expression
grlimgrtri (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻))
Distinct variable group:   𝑡,𝐻
Allowed substitution hints:   𝜑(𝑡)   𝑇(𝑡)   𝐹(𝑡)   𝐺(𝑡)
Proof of Theorem grlimgrtri
Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑔 𝑖 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grlimgrtri.t . . . 4 (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺))
2 eqid 2761 . . . . 5 (Vtx‘𝐺) = (Vtx‘𝐺)
3 eqid 2761 . . . . 5 (Edg‘𝐺) = (Edg‘𝐺)
42, 3grtriprop 49008 . . . 4 (𝑇 ∈ (GrTriangles‘𝐺) → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)∃𝑐 ∈ (Vtx‘𝐺)(𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
51, 4syl 18 . . 3 (𝜑 → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)∃𝑐 ∈ (Vtx‘𝐺)(𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
6 grlimgrtri.g . . . . . . 7 (𝜑 → 𝐺 ∈ USPGraph)
7 grlimgrtri.h . . . . . . 7 (𝜑 → 𝐻 ∈ USPGraph)
8 grlimgrtri.n . . . . . . 7 (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
96, 7, 83jca 1146 . . . . . 6 (𝜑 → (𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻)))
10 eqid 2761 . . . . . . 7 (Vtx‘𝐻) = (Vtx‘𝐻)
11 eqid 2761 . . . . . . 7 (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑣)
12 eqid 2761 . . . . . . 7 (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑣))
13 eqid 2761 . . . . . . 7 (Edg‘𝐻) = (Edg‘𝐻)
14 sseq1 3956 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)))
1514cbvrabv 3423 . . . . . . 7 {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)}
16 sseq1 3956 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))))
1716cbvrabv 3423 . . . . . . 7 {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))}
182, 10, 11, 12, 3, 13, 15, 17usgrlimprop 49060 . . . . . 6 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
19 eqidd 2762 . . . . . . . . . . . . . . 15 (𝑣 = 𝑎 → 𝑓 = 𝑓)
20 oveq2 7426 . . . . . . . . . . . . . . 15 (𝑣 = 𝑎 → (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑎))
21 fveq2 6883 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑎 → (𝐹‘𝑣) = (𝐹‘𝑎))
2221oveq2d 7434 . . . . . . . . . . . . . . 15 (𝑣 = 𝑎 → (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑎)))
2319, 20, 22f1oeq123d 6816 . . . . . . . . . . . . . 14 (𝑣 = 𝑎 → (𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎))))
24 eqidd 2762 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑎 → 𝑔 = 𝑔)
2520sseq2d 3963 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)))
2625rabbidv 3420 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)})
2722sseq2d 3963 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))))
2827rabbidv 3420 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))})
2924, 26, 28f1oeq123d 6816 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑎 → (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ↔ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}))
3026raleqdv 3320 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑎 → (∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ↔ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))
3129, 30anbi12d 644 . . . . . . . . . . . . . . 15 (𝑣 = 𝑎 → ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ↔ (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))))
3231exbidv 1954 . . . . . . . . . . . . . 14 (𝑣 = 𝑎 → (∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ↔ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))))
3323, 32anbi12d 644 . . . . . . . . . . . . 13 (𝑣 = 𝑎 → ((𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) ↔ (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
3433exbidv 1954 . . . . . . . . . . . 12 (𝑣 = 𝑎 → (∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) ↔ ∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
3534rspcv 3573 . . . . . . . . . . 11 (𝑎 ∈ (Vtx‘𝐺) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → ∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
36353ad2ant1 1151 . . . . . . . . . 10 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → ∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
3736adantl 487 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → ∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
38 tpex 7760 . . . . . . . . . . . . . . . 16 {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∈ V
3938a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∈ V)
40 f1of1 6821 . . . . . . . . . . . . . . . . . . 19 (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)))
41403ad2ant2 1152 . . . . . . . . . . . . . . . . . 18 (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)))
42413ad2ant2 1152 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)))
432clnbgrvtxel 48896 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (Vtx‘𝐺) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
44433ad2ant1 1151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
4544adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
46 simplr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (Vtx‘𝐺))
47 simpll 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑎 ∈ (Vtx‘𝐺))
48 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → {𝑎, 𝑏} ∈ (Edg‘𝐺))
492, 3predgclnbgrel 48906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
5046, 47, 48, 49syl3anc 1398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
51502a1d 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))))
5251ex 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))))
53523impd 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))
54533adant3 1150 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))
5554imp 412 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
56 simplr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (Vtx‘𝐺))
57 simpll 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑎 ∈ (Vtx‘𝐺))
58 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → {𝑎, 𝑐} ∈ (Edg‘𝐺))
592, 3predgclnbgrel 48906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
6056, 57, 58, 59syl3anc 1398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
6160a1d 26 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
6261ex 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
6362a1d 26 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))))
64633impd 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
65643adant2 1149 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
6665imp 412 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
6745, 55, 663jca 1146 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
6867ex 418 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
69682a1d 27 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (𝑇 = {𝑎, 𝑏, 𝑐} → ((♯‘𝑇) = 3 → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))))
70693impd 1367 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
7170a1d 26 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))))
7271adantl 487 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))))
73723imp 1128 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
74 3simpa 1166 . . . . . . . . . . . . . . . . . . 19 ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3))
75743ad2ant3 1153 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3))
7673, 75jca 521 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → ((𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)))
77 grtrimap 49015 . . . . . . . . . . . . . . . . 17 (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → (((𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)) → (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)))
7842, 76, 77sylc 66 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3))
79 tpeq1 4703 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦, 𝑧} = {(𝑓‘𝑎), 𝑦, 𝑧})
8079eqeq2d 2772 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑓‘𝑎) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧}))
81 preq1 4694 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦} = {(𝑓‘𝑎), 𝑦})
8281eleq1d 2846 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻)))
83 preq1 4694 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑧} = {(𝑓‘𝑎), 𝑧})
8483eleq1d 2846 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻)))
8582, 843anbi12d 1465 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑓‘𝑎) → (({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
8680, 853anbi13d 1466 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑓‘𝑎) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
87 tpeq2 4704 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦, 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧})
8887eqeq2d 2772 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧}))
89 preq2 4695 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦} = {(𝑓‘𝑎), (𝑓‘𝑏)})
9089eleq1d 2846 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻)))
91 preq1 4694 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑓‘𝑏) → {𝑦, 𝑧} = {(𝑓‘𝑏), 𝑧})
9291eleq1d 2846 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑓‘𝑏) → ({𝑦, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))
9390, 923anbi13d 1466 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))))
9488, 933anbi13d 1466 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))))
95 tpeq3 4705 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)})
9695eqeq2d 2772 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}))
97 preq2 4695 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑐)})
9897eleq1d 2846 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
99 preq2 4695 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑏), 𝑧} = {(𝑓‘𝑏), (𝑓‘𝑐)})
10099eleq1d 2846 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
10198, 1003anbi23d 1467 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
10296, 1013anbi13d 1466 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))))
10310clnbgrisvtx 48897 . . . . . . . . . . . . . . . . . . . 20 ((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
1041033ad2ant1 1151 . . . . . . . . . . . . . . . . . . 19 (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
1051043ad2ant1 1151 . . . . . . . . . . . . . . . . . 18 ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
106105adantl 487 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
10710clnbgrisvtx 48897 . . . . . . . . . . . . . . . . . . . 20 ((𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
1081073ad2ant2 1152 . . . . . . . . . . . . . . . . . . 19 (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
1091083ad2ant1 1151 . . . . . . . . . . . . . . . . . 18 ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
110109adantl 487 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
11110clnbgrisvtx 48897 . . . . . . . . . . . . . . . . . . . 20 ((𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
1121113ad2ant3 1153 . . . . . . . . . . . . . . . . . . 19 (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
1131123ad2ant1 1151 . . . . . . . . . . . . . . . . . 18 ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
114113adantl 487 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
115 eqidd 2762 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)})
116 fveq2 6883 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = (𝑓 “ 𝑇) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
117116eqcoms 2769 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
1181173ad2ant2 1152 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
119 simp3 1156 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘(𝑓 “ 𝑇)) = 3)
120118, 119eqtrd 2796 . . . . . . . . . . . . . . . . . . 19 ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3)
121120adantl 487 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3)
122 uspgruhgr 29758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
1236, 122syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝐺 ∈ UHGraph)
124123adantr 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → 𝐺 ∈ UHGraph)
125 simp3 1156 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))
126124, 125anim12i 625 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
1271263adant2 1149 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
128127adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
129 eqid 2761 . . . . . . . . . . . . . . . . . . . . 21 (𝐺 ClNeighbVtx 𝑎) = (𝐺 ClNeighbVtx 𝑎)
130 eqid 2761 . . . . . . . . . . . . . . . . . . . . 21 {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}
1312, 129, 3, 130grlimgrtrilem1 49068 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}))
132128, 131syl 18 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → ({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}))
133 eqid 2761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐻 ClNeighbVtx (𝐹‘𝑎)) = (𝐻 ClNeighbVtx (𝐹‘𝑎))
134 eqid 2761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}
1352, 129, 3, 130, 133, 13, 134grlimgrtrilem2 49069 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻))
1361353expia 1139 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → ({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} → {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻)))
1372, 129, 3, 130, 133, 13, 134grlimgrtrilem2 49069 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻))
1381373expia 1139 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → ({𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} → {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
1392, 129, 3, 130, 133, 13, 134grlimgrtrilem2 49069 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))
1401393expia 1139 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → ({𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
141136, 138, 1403anim123d 1471 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
142141anasss 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
143142ancoms 464 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎))) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
1441433adant3 1150 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
1451443ad2ant2 1152 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
146145adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
147132, 146mpd 16 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
148115, 121, 1473jca 1146 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
14986, 94, 102, 106, 110, 114, 1483rspcedvdw 3594 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
15078, 149mpdan 700 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
151 eqeq1 2765 . . . . . . . . . . . . . . . . . 18 (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (𝑡 = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧}))
152 fveqeq2 6892 . . . . . . . . . . . . . . . . . 18 (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((♯‘𝑡) = 3 ↔ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3))
153151, 1523anbi12d 1465 . . . . . . . . . . . . . . . . 17 (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
154153rexbidv 3187 . . . . . . . . . . . . . . . 16 (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
1551542rexbidv 3228 . . . . . . . . . . . . . . 15 (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
15639, 150, 155spcedv 3553 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
1571563exp 1137 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))
1581573expd 1372 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))))
159158exlimdv 1966 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))))
160159impcomd 417 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))))
161160exlimdv 1966 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))))
16237, 161syld 48 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))))
163162com13 89 . . . . . . 7 (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))))
164163imp 412 . . . . . 6 ((𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))) → ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))
1659, 18, 1643syl 19 . . . . 5 (𝜑 → ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))
166165anabsi5 682 . . . 4 ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
167166rexlimdvvva 3221 . . 3 (𝜑 → (∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)∃𝑐 ∈ (Vtx‘𝐺)(𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
1685, 167mpd 16 . 2 (𝜑 → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
16910, 13isgrtri 49010 . . 3 (𝑡 ∈ (GrTriangles‘𝐻) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
170169exbii 1881 . 2 (∃𝑡 𝑡 ∈ (GrTriangles‘𝐻) ↔ ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
171168, 170sylibr 237 1 (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  {crab 3413  Vcvv 3451   ⊆ wss 3899  {cpr 4586  {ctp 4588   “ cima 5654  –1-1→wf1 6534  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7418  3c3 12391  ♯chash 14467  Vtxcvtx 29567  Edgcedg 29618  UHGraphcuhgr 29627  USPGraphcuspgr 29722   ClNeighbVtx cclnbgr 48885  GrTrianglescgrtri 49004   GraphLocIso cgrlim 49043
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-2o 8470  df-3o 8471  df-oadd 8473  df-er 8710  df-map 8842  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-dju 9975  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-2 12398  df-3 12399  df-n0 12600  df-xnn0 12673  df-z 12687  df-uz 12959  df-fz 13633  df-fzo 13782  df-hash 14468  df-vtx 29569  df-iedg 29570  df-edg 29619  df-uhgr 29629  df-upgr 29653  df-uspgr 29724  df-clnbgr 48886  df-isubgr 48928  df-grim 48945  df-gric 48948  df-grtri 49005  df-grlim 49045
This theorem is used by:  usgrexmpl12ngrlic  49106
  Copyright terms: Public domain W3C validator