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 2strstr1 𝐺 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 slotsbaseefdif ( 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 syl5eq ( ( 𝑉𝑋𝐸𝑌𝑆 ≠ ( .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 syl5eq ( ( 𝑉𝑋𝐸𝑌𝑆 ≠ ( .ef ‘ ndx ) ) → ( .ef ‘ 𝐺 ) = ∅ )
36 10 35 eqtrd ( ( 𝑉𝑋𝐸𝑌𝑆 ≠ ( .ef ‘ ndx ) ) → ( iEdg ‘ 𝐺 ) = ∅ )