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

Metamath Proof Explorer

Theorem fodomfi2

Description: Onto functions define dominance when a finite number of choices need to be made. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Assertion fodomfi2 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 fofn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
2 1 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐹 Fn 𝐴 )
3 forn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
4 eqimss2 ⊢ ( ran 𝐹 = 𝐵 → 𝐵 ⊆ ran 𝐹 )
5 3 4 syl ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ⊆ ran 𝐹 )
6 5 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ⊆ ran 𝐹 )
7 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ Fin )
8 fipreima ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹 ∧ 𝐵 ∈ Fin ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝐹 “ 𝑥 ) = 𝐵 )
9 2 6 7 8 syl3anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝐹 “ 𝑥 ) = 𝐵 )
10 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ Fin )
11 10 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ Fin )
12 finnum ⊢ ( 𝑥 ∈ Fin → 𝑥 ∈ dom card )
13 11 12 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ dom card )
14 simpl3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 : 𝐴 –onto→ 𝐵 )
15 fofun ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Fun 𝐹 )
16 14 15 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Fun 𝐹 )
17 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ 𝒫 𝐴 )
18 17 elpwid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ⊆ 𝐴 )
19 18 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ⊆ 𝐴 )
20 fof ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
21 fdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
22 14 20 21 3syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → dom 𝐹 = 𝐴 )
23 19 22 sseqtrrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ⊆ dom 𝐹 )
24 fores ⊢ ( ( Fun 𝐹 ∧ 𝑥 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –onto→ ( 𝐹 “ 𝑥 ) )
25 16 23 24 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –onto→ ( 𝐹 “ 𝑥 ) )
26 fodomnum ⊢ ( 𝑥 ∈ dom card → ( ( 𝐹 ↾ 𝑥 ) : 𝑥 –onto→ ( 𝐹 “ 𝑥 ) → ( 𝐹 “ 𝑥 ) ≼ 𝑥 ) )
27 13 25 26 sylc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 “ 𝑥 ) ≼ 𝑥 )
28 simpl1 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐴 ∈ 𝑉 )
29 ssdomg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴 ) )
30 28 19 29 sylc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ≼ 𝐴 )
31 domtr ⊢ ( ( ( 𝐹 “ 𝑥 ) ≼ 𝑥 ∧ 𝑥 ≼ 𝐴 ) → ( 𝐹 “ 𝑥 ) ≼ 𝐴 )
32 27 30 31 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 “ 𝑥 ) ≼ 𝐴 )
33 breq1 ⊢ ( ( 𝐹 “ 𝑥 ) = 𝐵 → ( ( 𝐹 “ 𝑥 ) ≼ 𝐴 ↔ 𝐵 ≼ 𝐴 ) )
34 32 33 syl5ibcom ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 “ 𝑥 ) = 𝐵 → 𝐵 ≼ 𝐴 ) )
35 34 rexlimdva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ( ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝐹 “ 𝑥 ) = 𝐵 → 𝐵 ≼ 𝐴 ) )
36 9 35 mpd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 )