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→ 𝐵 ) → 𝐵 ≼ 𝐴 )