Step |
Hyp |
Ref |
Expression |
1 |
|
structgrssvtx.g |
⊢ ( 𝜑 → 𝐺 Struct 𝑋 ) |
2 |
|
structgrssvtx.v |
⊢ ( 𝜑 → 𝑉 ∈ 𝑌 ) |
3 |
|
structgrssvtx.e |
⊢ ( 𝜑 → 𝐸 ∈ 𝑍 ) |
4 |
|
structgrssvtx.s |
⊢ ( 𝜑 → { 〈 ( Base ‘ ndx ) , 𝑉 〉 , 〈 ( .ef ‘ ndx ) , 𝐸 〉 } ⊆ 𝐺 ) |
5 |
|
fvexd |
⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ V ) |
6 |
|
fvexd |
⊢ ( 𝜑 → ( .ef ‘ ndx ) ∈ V ) |
7 |
|
structex |
⊢ ( 𝐺 Struct 𝑋 → 𝐺 ∈ V ) |
8 |
1 7
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ V ) |
9 |
|
slotsbaseefdif |
⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx ) |
10 |
9
|
a1i |
⊢ ( 𝜑 → ( Base ‘ ndx ) ≠ ( .ef ‘ ndx ) ) |
11 |
5 6 2 3 8 10 4
|
hashdmpropge2 |
⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) ) |