Metamath Proof Explorer

Theorem 1vwmgr

Description: Every graph with one vertex (which may be connect with itself by (multiple) loops!) is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Assertion 1vwmgr ( ( 𝐴 ∈ 𝑋 ∧ 𝑉 = { 𝐴 } ) → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 ral0 ⊢ ∀ 𝑣 ∈ ∅ ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )
2 sneq ⊢ ( ℎ = 𝐴 → { ℎ } = { 𝐴 } )
3 2 difeq2d ⊢ ( ℎ = 𝐴 → ( { 𝐴 } ∖ { ℎ } ) = ( { 𝐴 } ∖ { 𝐴 } ) )
4 difid ⊢ ( { 𝐴 } ∖ { 𝐴 } ) = ∅
5 3 4 eqtrdi ⊢ ( ℎ = 𝐴 → ( { 𝐴 } ∖ { ℎ } ) = ∅ )
6 preq2 ⊢ ( ℎ = 𝐴 → { 𝑣 , ℎ } = { 𝑣 , 𝐴 } )
7 6 eleq1d ⊢ ( ℎ = 𝐴 → ( { 𝑣 , ℎ } ∈ 𝐸 ↔ { 𝑣 , 𝐴 } ∈ 𝐸 ) )
8 reueq1 ⊢ ( ( { 𝐴 } ∖ { ℎ } ) = ( { 𝐴 } ∖ { 𝐴 } ) → ( ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
9 3 8 syl ⊢ ( ℎ = 𝐴 → ( ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
10 7 9 anbi12d ⊢ ( ℎ = 𝐴 → ( ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
11 5 10 raleqbidv ⊢ ( ℎ = 𝐴 → ( ∀ 𝑣 ∈ ( { 𝐴 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ ∅ ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
12 11 rexsng ⊢ ( 𝐴 ∈ 𝑋 → ( ∃ ℎ ∈ { 𝐴 } ∀ 𝑣 ∈ ( { 𝐴 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ ∅ ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
13 1 12 mpbiri ⊢ ( 𝐴 ∈ 𝑋 → ∃ ℎ ∈ { 𝐴 } ∀ 𝑣 ∈ ( { 𝐴 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
14 13 adantr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑉 = { 𝐴 } ) → ∃ ℎ ∈ { 𝐴 } ∀ 𝑣 ∈ ( { 𝐴 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
15 difeq1 ⊢ ( 𝑉 = { 𝐴 } → ( 𝑉 ∖ { ℎ } ) = ( { 𝐴 } ∖ { ℎ } ) )
16 reueq1 ⊢ ( ( 𝑉 ∖ { ℎ } ) = ( { 𝐴 } ∖ { ℎ } ) → ( ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
17 15 16 syl ⊢ ( 𝑉 = { 𝐴 } → ( ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
18 17 anbi2d ⊢ ( 𝑉 = { 𝐴 } → ( ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
19 15 18 raleqbidv ⊢ ( 𝑉 = { 𝐴 } → ( ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ ( { 𝐴 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
20 19 rexeqbi1dv ⊢ ( 𝑉 = { 𝐴 } → ( ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∃ ℎ ∈ { 𝐴 } ∀ 𝑣 ∈ ( { 𝐴 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
21 20 adantl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑉 = { 𝐴 } ) → ( ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∃ ℎ ∈ { 𝐴 } ∀ 𝑣 ∈ ( { 𝐴 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
22 14 21 mpbird ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑉 = { 𝐴 } ) → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )