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→ ( 𝑅 ∪ { 𝑌 } ) )