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

Metamath Proof Explorer

Theorem fidomdm

Description: Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion fidomdm ( 𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹 )

Proof

Step Hyp Ref Expression
1 dmresv ⊢ dom ( 𝐹 ↾ V ) = dom 𝐹
2 finresfin ⊢ ( 𝐹 ∈ Fin → ( 𝐹 ↾ V ) ∈ Fin )
3 fvex ⊢ ( 1st ‘ 𝑥 ) ∈ V
4 eqid ⊢ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) )
5 3 4 fnmpti ⊢ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) Fn ( 𝐹 ↾ V )
6 dffn4 ⊢ ( ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) Fn ( 𝐹 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) )
7 5 6 mpbi ⊢ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) )
8 relres ⊢ Rel ( 𝐹 ↾ V )
9 reldm ⊢ ( Rel ( 𝐹 ↾ V ) → dom ( 𝐹 ↾ V ) = ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) )
10 foeq3 ⊢ ( dom ( 𝐹 ↾ V ) = ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) → ( ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ dom ( 𝐹 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) ) )
11 8 9 10 mp2b ⊢ ( ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ dom ( 𝐹 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) )
12 7 11 mpbir ⊢ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ dom ( 𝐹 ↾ V )
13 fodomfi ⊢ ( ( ( 𝐹 ↾ V ) ∈ Fin ∧ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ dom ( 𝐹 ↾ V ) ) → dom ( 𝐹 ↾ V ) ≼ ( 𝐹 ↾ V ) )
14 2 12 13 sylancl ⊢ ( 𝐹 ∈ Fin → dom ( 𝐹 ↾ V ) ≼ ( 𝐹 ↾ V ) )
15 resss ⊢ ( 𝐹 ↾ V ) ⊆ 𝐹
16 ssdomg ⊢ ( 𝐹 ∈ Fin → ( ( 𝐹 ↾ V ) ⊆ 𝐹 → ( 𝐹 ↾ V ) ≼ 𝐹 ) )
17 15 16 mpi ⊢ ( 𝐹 ∈ Fin → ( 𝐹 ↾ V ) ≼ 𝐹 )
18 domtr ⊢ ( ( dom ( 𝐹 ↾ V ) ≼ ( 𝐹 ↾ V ) ∧ ( 𝐹 ↾ V ) ≼ 𝐹 ) → dom ( 𝐹 ↾ V ) ≼ 𝐹 )
19 14 17 18 syl2anc ⊢ ( 𝐹 ∈ Fin → dom ( 𝐹 ↾ V ) ≼ 𝐹 )
20 1 19 eqbrtrrid ⊢ ( 𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹 )