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 𝐹𝐹 )