Metamath Proof Explorer


Theorem isubgr3stgrlem1

Description: Lemma 1 for isubgr3stgr . (Contributed by AV, 16-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v 𝑉 = ( Vtx ‘ 𝐺 )
isubgr3stgr.u 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
isubgr3stgr.c 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
isubgr3stgr.f 𝐹 = ( 𝐻 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } )
Assertion isubgr3stgrlem1 ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → 𝐹 : 𝐶1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgr3stgr.u 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
3 isubgr3stgr.c 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
4 isubgr3stgr.f 𝐹 = ( 𝐻 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } )
5 f1oeq2 ( 𝑈 = ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐻 : 𝑈1-1-onto𝑅𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto𝑅 ) )
6 2 5 ax-mp ( 𝐻 : 𝑈1-1-onto𝑅𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto𝑅 )
7 6 biimpi ( 𝐻 : 𝑈1-1-onto𝑅𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto𝑅 )
8 7 3ad2ant1 ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → 𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto𝑅 )
9 simpl ( ( 𝑌𝑊𝑌𝑅 ) → 𝑌𝑊 )
10 9 anim2i ( ( 𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → ( 𝑋𝑉𝑌𝑊 ) )
11 10 3adant1 ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → ( 𝑋𝑉𝑌𝑊 ) )
12 nbgrnself2 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 )
13 12 a1i ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) )
14 simp3r ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → 𝑌𝑅 )
15 4 f1ounsn ( ( 𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto𝑅 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) ∧ 𝑌𝑅 ) ) → 𝐹 : ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) –1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) )
16 8 11 13 14 15 syl112anc ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → 𝐹 : ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) –1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) )
17 1 dfclnbgr4 ( 𝑋𝑉 → ( 𝐺 ClNeighbVtx 𝑋 ) = ( { 𝑋 } ∪ ( 𝐺 NeighbVtx 𝑋 ) ) )
18 17 3ad2ant2 ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → ( 𝐺 ClNeighbVtx 𝑋 ) = ( { 𝑋 } ∪ ( 𝐺 NeighbVtx 𝑋 ) ) )
19 uncom ( { 𝑋 } ∪ ( 𝐺 NeighbVtx 𝑋 ) ) = ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } )
20 18 19 eqtrdi ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → ( 𝐺 ClNeighbVtx 𝑋 ) = ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) )
21 3 20 eqtrid ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → 𝐶 = ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) )
22 21 f1oeq2d ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → ( 𝐹 : 𝐶1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) ↔ 𝐹 : ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) –1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) ) )
23 16 22 mpbird ( ( 𝐻 : 𝑈1-1-onto𝑅𝑋𝑉 ∧ ( 𝑌𝑊𝑌𝑅 ) ) → 𝐹 : 𝐶1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) )