This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem structiedg0val

Description: The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypotheses structvtxvallem.s ⊢ 𝑆 ∈ ℕ
structvtxvallem.b ⊢ ( Base ‘ ndx ) < 𝑆
structvtxvallem.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
Assertion structiedg0val ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( iEdg ‘ 𝐺 ) = ∅ )

Proof

Step Hyp Ref Expression
1 structvtxvallem.s ⊢ 𝑆 ∈ ℕ
2 structvtxvallem.b ⊢ ( Base ‘ ndx ) < 𝑆
3 structvtxvallem.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
4 3 2 1 2strstr ⊢ 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑆 ⟩
5 structn0fun ⊢ ( 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑆 ⟩ → Fun ( 𝐺 ∖ { ∅ } ) )
6 1 2 3 structvtxvallem ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
7 funiedgdmge2val ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
8 5 6 7 syl2an ⊢ ( ( 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑆 ⟩ ∧ ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
9 4 8 mpan ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
10 9 3adant3 ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
11 prex ⊢ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } ∈ V
12 11 a1i ⊢ ( 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } ∈ V )
13 3 12 eqeltrid ⊢ ( 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } → 𝐺 ∈ V )
14 edgfndxid ⊢ ( 𝐺 ∈ V → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )
15 3 13 14 mp2b ⊢ ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) )
16 basendxnedgfndx ⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
17 16 nesymi ⊢ ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx )
18 17 a1i ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx ) )
19 neneq ⊢ ( 𝑆 ≠ ( .ef ‘ ndx ) → ¬ 𝑆 = ( .ef ‘ ndx ) )
20 eqcom ⊢ ( ( .ef ‘ ndx ) = 𝑆 ↔ 𝑆 = ( .ef ‘ ndx ) )
21 19 20 sylnibr ⊢ ( 𝑆 ≠ ( .ef ‘ ndx ) → ¬ ( .ef ‘ ndx ) = 𝑆 )
22 21 3ad2ant3 ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( .ef ‘ ndx ) = 𝑆 )
23 ioran ⊢ ( ¬ ( ( .ef ‘ ndx ) = ( Base ‘ ndx ) ∨ ( .ef ‘ ndx ) = 𝑆 ) ↔ ( ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx ) ∧ ¬ ( .ef ‘ ndx ) = 𝑆 ) )
24 18 22 23 sylanbrc ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( ( .ef ‘ ndx ) = ( Base ‘ ndx ) ∨ ( .ef ‘ ndx ) = 𝑆 ) )
25 fvex ⊢ ( .ef ‘ ndx ) ∈ V
26 25 elpr ⊢ ( ( .ef ‘ ndx ) ∈ { ( Base ‘ ndx ) , 𝑆 } ↔ ( ( .ef ‘ ndx ) = ( Base ‘ ndx ) ∨ ( .ef ‘ ndx ) = 𝑆 ) )
27 24 26 sylnibr ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( .ef ‘ ndx ) ∈ { ( Base ‘ ndx ) , 𝑆 } )
28 3 dmeqi ⊢ dom 𝐺 = dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
29 dmpropg ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } = { ( Base ‘ ndx ) , 𝑆 } )
30 29 3adant3 ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } = { ( Base ‘ ndx ) , 𝑆 } )
31 28 30 eqtrid ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → dom 𝐺 = { ( Base ‘ ndx ) , 𝑆 } )
32 27 31 neleqtrrd ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( .ef ‘ ndx ) ∈ dom 𝐺 )
33 ndmfv ⊢ ( ¬ ( .ef ‘ ndx ) ∈ dom 𝐺 → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ∅ )
34 32 33 syl ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ∅ )
35 15 34 eqtrid ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( .ef ‘ 𝐺 ) = ∅ )
36 10 35 eqtrd ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( iEdg ‘ 𝐺 ) = ∅ )