Theorem fodomfi 4709

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 4944 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof.

Assertion

Ref	Expression
fodomfi	⊢ ((A ∈ Fin ⋀ F:A–onto→B) → B ≼ A)

Proof of Theorem fodomfi

Step	Hyp	Ref	Expression
1		domentr 4562	. . . . . 6 ⊢ ((B ≼ m ⋀ m ≈ A) → B ≼ A)
2		fex 3759	. . . . . . . . . 10 ⊢ ((F:A–→B ⋀ A ∈ V) → F ∈ V)
3	2	ancoms 438	. . . . . . . . 9 ⊢ ((A ∈ V ⋀ F:A–→B) → F ∈ V)
4		relen 4513	. . . . . . . . . 10 ⊢ Rel ≈
5	4	brrelexi 3291	. . . . . . . . 9 ⊢ (A ≈ m → A ∈ V)
6		fof 3779	. . . . . . . . 9 ⊢ (F:A–onto→B → F:A–→B)
7	3, 5, 6	syl2an 456	. . . . . . . 8 ⊢ ((A ≈ m ⋀ F:A–onto→B) → F ∈ V)
8	7	adantl 388	. . . . . . 7 ⊢ ((m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B)) → F ∈ V)
9		visset 1859	. . . . . . . . . . . . . 14 ⊢ g ∈ V
10		coexg 3629	. . . . . . . . . . . . . 14 ⊢ ((F ∈ V ⋀ g ∈ V) → (F ∘ g) ∈ V)
11	9, 10	mpan2 700	. . . . . . . . . . . . 13 ⊢ (F ∈ V → (F ∘ g) ∈ V)
12		foeq1 3775	. . . . . . . . . . . . . 14 ⊢ (f = (F ∘ g) → (f:m–onto→B ↔ (F ∘ g):m–onto→B))
13	12	cla4egv 1909	. . . . . . . . . . . . 13 ⊢ ((F ∘ g) ∈ V → ((F ∘ g):m–onto→B → ∃f f:m–onto→B))
14	11, 13	syl 10	. . . . . . . . . . . 12 ⊢ (F ∈ V → ((F ∘ g):m–onto→B → ∃f f:m–onto→B))
15		visset 1859	. . . . . . . . . . . . . . . 16 ⊢ m ∈ V
16		fornex 3787	. . . . . . . . . . . . . . . 16 ⊢ (m ∈ V → (f:m–onto→B → B ∈ V))
17	15, 16	ax-mp 7	. . . . . . . . . . . . . . 15 ⊢ (f:m–onto→B → B ∈ V)
18	17	19.23aiv 1333	. . . . . . . . . . . . . 14 ⊢ (∃f f:m–onto→B → B ∈ V)
19		foeq3 3777	. . . . . . . . . . . . . . . . . 18 ⊢ (x = B → (f:m–onto→x ↔ f:m–onto→B))
20	19	exbidv 1317	. . . . . . . . . . . . . . . . 17 ⊢ (x = B → (∃f f:m–onto→x ↔ ∃f f:m–onto→B))
21		breq1 2695	. . . . . . . . . . . . . . . . 17 ⊢ (x = B → (x ≼ m ↔ B ≼ m))
22	20, 21	imbi12d 629	. . . . . . . . . . . . . . . 16 ⊢ (x = B → ((∃f f:m–onto→x → x ≼ m) ↔ (∃f f:m–onto→B → B ≼ m)))
23	22	cla4gv 1908	. . . . . . . . . . . . . . 15 ⊢ (B ∈ V → (∀x(∃f f:m–onto→x → x ≼ m) → (∃f f:m–onto→B → B ≼ m)))
24		foeq2 3776	. . . . . . . . . . . . . . . . . . 19 ⊢ (m = ∅ → (f:m–onto→x ↔ f:∅–onto→x))
25	24	exbidv 1317	. . . . . . . . . . . . . . . . . 18 ⊢ (m = ∅ → (∃f f:m–onto→x ↔ ∃f f:∅–onto→x))
26		breq2 2696	. . . . . . . . . . . . . . . . . 18 ⊢ (m = ∅ → (x ≼ m ↔ x ≼ ∅))
27	25, 26	imbi12d 629	. . . . . . . . . . . . . . . . 17 ⊢ (m = ∅ → ((∃f f:m–onto→x → x ≼ m) ↔ (∃f f:∅–onto→x → x ≼ ∅)))
28	27	albidv 1316	. . . . . . . . . . . . . . . 16 ⊢ (m = ∅ → (∀x(∃f f:m–onto→x → x ≼ m) ↔ ∀x(∃f f:∅–onto→x → x ≼ ∅)))
29		foeq2 3776	. . . . . . . . . . . . . . . . . . 19 ⊢ (m = k → (f:m–onto→x ↔ f:k–onto→x))
30	29	exbidv 1317	. . . . . . . . . . . . . . . . . 18 ⊢ (m = k → (∃f f:m–onto→x ↔ ∃f f:k–onto→x))
31		breq2 2696	. . . . . . . . . . . . . . . . . 18 ⊢ (m = k → (x ≼ m ↔ x ≼ k))
32	30, 31	imbi12d 629	. . . . . . . . . . . . . . . . 17 ⊢ (m = k → ((∃f f:m–onto→x → x ≼ m) ↔ (∃f f:k–onto→x → x ≼ k)))
33	32	albidv 1316	. . . . . . . . . . . . . . . 16 ⊢ (m = k → (∀x(∃f f:m–onto→x → x ≼ m) ↔ ∀x(∃f f:k–onto→x → x ≼ k)))
34		foeq2 3776	. . . . . . . . . . . . . . . . . . 19 ⊢ (m = suc k → (f:m–onto→x ↔ f:suc k–onto→x))
35	34	exbidv 1317	. . . . . . . . . . . . . . . . . 18 ⊢ (m = suc k → (∃f f:m–onto→x ↔ ∃f f:suc k–onto→x))
36		breq2 2696	. . . . . . . . . . . . . . . . . 18 ⊢ (m = suc k → (x ≼ m ↔ x ≼ suc k))
37	35, 36	imbi12d 629	. . . . . . . . . . . . . . . . 17 ⊢ (m = suc k → ((∃f f:m–onto→x → x ≼ m) ↔ (∃f f:suc k–onto→x → x ≼ suc k)))
38	37	albidv 1316	. . . . . . . . . . . . . . . 16 ⊢ (m = suc k → (∀x(∃f f:m–onto→x → x ≼ m) ↔ ∀x(∃f f:suc k–onto→x → x ≼ suc k)))
39		fo00 3826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f:∅–onto→x ↔ (f = ∅ ⋀ x = ∅))
40	39	pm3.27bi 324	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:∅–onto→x → x = ∅)
41		0dom 4609	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ≼ ∅
42	40, 41	syl6eqbr 2725	. . . . . . . . . . . . . . . . . 18 ⊢ (f:∅–onto→x → x ≼ ∅)
43	42	19.23aiv 1333	. . . . . . . . . . . . . . . . 17 ⊢ (∃f f:∅–onto→x → x ≼ ∅)
44	43	ax-gen 999	. . . . . . . . . . . . . . . 16 ⊢ ∀x(∃f f:∅–onto→x → x ≼ ∅)
45		fofn 3781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc k–onto→x → f Fn suc k)
46		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ k ∈ V
47	46	sucid 3051	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ k ∈ suc k
48		fnsnfv 3878	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f Fn suc k ⋀ k ∈ suc k) → {(f ‘k)} = (f “ {k}))
49	47, 48	mpan2 700	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f Fn suc k → {(f ‘k)} = (f “ {k}))
50	45, 49	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc k–onto→x → {(f ‘k)} = (f “ {k}))
51	50	uneq2d 2236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc k–onto→x → ((f “ k) ∪ {(f ‘k)}) = ((f “ k) ∪ (f “ {k})))
52		foima 3784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc k–onto→x → (f “ suc k) = x)
53		df-suc 2981	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ suc k = (k ∪ {k})
54	53	imaeq2i 3494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f “ suc k) = (f “ (k ∪ {k}))
55		imaundi 3545	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f “ (k ∪ {k})) = ((f “ k) ∪ (f “ {k}))
56	54, 55	eqtr2i 1539	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f “ k) ∪ (f “ {k})) = (f “ suc k)
57	52, 56	syl5eq 1562	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc k–onto→x → ((f “ k) ∪ (f “ {k})) = x)
58	51, 57	eqtrd 1550	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc k–onto→x → ((f “ k) ∪ {(f ‘k)}) = x)
59	58	adantl 388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → ((f “ k) ∪ {(f ‘k)}) = x)
60		snex 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {(f ‘k)} ∈ V
61		snex 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {k} ∈ V
62	46, 60, 61	undom 4579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((f “ k) ≼ k ⋀ {(f ‘k)} ≼ {k}) ⋀ (k ∩ {k}) = ∅) → ((f “ k) ∪ {(f ‘k)}) ≼ (k ∪ {k}))
63		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ f ∈ V
64		imaexg 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f ∈ V → (f “ k) ∈ V)
65	63, 64	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f “ k) ∈ V
66		foeq3 3777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (y = (f “ k) → (g:k–onto→y ↔ g:k–onto→(f “ k)))
67	66	exbidv 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (y = (f “ k) → (∃g g:k–onto→y ↔ ∃g g:k–onto→(f “ k)))
68		breq1 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (y = (f “ k) → (y ≼ k ↔ (f “ k) ≼ k))
69	67, 68	imbi12d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (y = (f “ k) → ((∃g g:k–onto→y → y ≼ k) ↔ (∃g g:k–onto→(f “ k) → (f “ k) ≼ k)))
70	65, 69	cla4v 1914	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀y(∃g g:k–onto→y → y ≼ k) → (∃g g:k–onto→(f “ k) → (f “ k) ≼ k))
71	70	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀y(∃g g:k–onto→y → y ≼ k) ⋀ ∃g g:k–onto→(f “ k)) → (f “ k) ≼ k)
72		fores 3789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Fun f ⋀ k ⊆ dom f) → (f ↾ k):k–onto→(f “ k))
73		fofun 3780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f:suc k–onto→x → Fun f)
74		fof 3779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f:suc k–onto→x → f:suc k–→x)
75		sssucid 3050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ k ⊆ suc k
76		fdm 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f:suc k–→x → dom f = suc k)
77	76	sseq2d 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (f:suc k–→x → (k ⊆ dom f ↔ k ⊆ suc k))
78	75, 77	mpbiri 192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f:suc k–→x → k ⊆ dom f)
79	74, 78	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f:suc k–onto→x → k ⊆ dom f)
80	72, 73, 79	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (f:suc k–onto→x → (f ↾ k):k–onto→(f “ k))
81		resexg 3484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f ∈ V → (f ↾ k) ∈ V)
82	63, 81	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f ↾ k) ∈ V
83		foeq1 3775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (g = (f ↾ k) → (g:k–onto→(f “ k) ↔ (f ↾ k):k–onto→(f “ k)))
84	82, 83	cla4ev 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f ↾ k):k–onto→(f “ k) → ∃g g:k–onto→(f “ k))
85	80, 84	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc k–onto→x → ∃g g:k–onto→(f “ k))
86	71, 85	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀y(∃g g:k–onto→y → y ≼ k) ⋀ f:suc k–onto→x) → (f “ k) ≼ k)
87	86	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → (f “ k) ≼ k)
88		fvex 3843	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f ‘k) ∈ V
89		en2sn 4572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((f ‘k) ∈ V ⋀ k ∈ V) → {(f ‘k)} ≈ {k})
90	88, 46, 89	mp2an 701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {(f ‘k)} ≈ {k}
91		endom 4526	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({(f ‘k)} ≈ {k} → {(f ‘k)} ≼ {k})
92	90, 91	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {(f ‘k)} ≼ {k}
93	87, 92	jctir 291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → ((f “ k) ≼ k ⋀ {(f ‘k)} ≼ {k}))
94		nnord 3227	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (k ∈ ω → Ord k)
95		orddisj 3013	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord k → (k ∩ {k}) = ∅)
96	94, 95	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (k ∈ ω → (k ∩ {k}) = ∅)
97	96	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → (k ∩ {k}) = ∅)
98	62, 93, 97	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → ((f “ k) ∪ {(f ‘k)}) ≼ (k ∪ {k}))
99	59, 98	eqbrtrrd 2710	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → x ≼ (k ∪ {k}))
100	99, 53	syl6breqr 2728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → x ≼ suc k)
101	100	ex 371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) → (f:suc k–onto→x → x ≼ suc k))
102	101	19.23adv 1251	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) → (∃f f:suc k–onto→x → x ≼ suc k))
103	102	ex 371	. . . . . . . . . . . . . . . . . 18 ⊢ (k ∈ ω → (∀y(∃g g:k–onto→y → y ≼ k) → (∃f f:suc k–onto→x → x ≼ suc k)))
104	103	19.21adv 1326	. . . . . . . . . . . . . . . . 17 ⊢ (k ∈ ω → (∀y(∃g g:k–onto→y → y ≼ k) → ∀x(∃f f:suc k–onto→x → x ≼ suc k)))
105		foeq3 3777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = y → (f:k–onto→x ↔ f:k–onto→y))
106	105	exbidv 1317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = y → (∃f f:k–onto→x ↔ ∃f f:k–onto→y))
107		foeq1 3775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f = g → (f:k–onto→y ↔ g:k–onto→y))
108	107	cbvexv 1353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃f f:k–onto→y ↔ ∃g g:k–onto→y)
109	106, 108	syl6bb 539	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → (∃f f:k–onto→x ↔ ∃g g:k–onto→y))
110		breq1 2695	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → (x ≼ k ↔ y ≼ k))
111	109, 110	imbi12d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (x = y → ((∃f f:k–onto→x → x ≼ k) ↔ (∃g g:k–onto→y → y ≼ k)))
112	111	cbvalv 1352	. . . . . . . . . . . . . . . . 17 ⊢ (∀x(∃f f:k–onto→x → x ≼ k) ↔ ∀y(∃g g:k–onto→y → y ≼ k))
113	104, 112	syl5ib 204	. . . . . . . . . . . . . . . 16 ⊢ (k ∈ ω → (∀x(∃f f:k–onto→x → x ≼ k) → ∀x(∃f f:suc k–onto→x → x ≼ suc k)))
114	28, 33, 38, 44, 113	finds1 3247	. . . . . . . . . . . . . . 15 ⊢ (m ∈ ω → ∀x(∃f f:m–onto→x → x ≼ m))
115	23, 114	syl5 21	. . . . . . . . . . . . . 14 ⊢ (B ∈ V → (m ∈ ω → (∃f f:m–onto→B → B ≼ m)))
116	18, 115	syl 10	. . . . . . . . . . . . 13 ⊢ (∃f f:m–onto→B → (m ∈ ω → (∃f f:m–onto→B → B ≼ m)))
117	116	pm2.43b 67	. . . . . . . . . . . 12 ⊢ (m ∈ ω → (∃f f:m–onto→B → B ≼ m))
118	14, 117	sylan9 470	. . . . . . . . . . 11 ⊢ ((F ∈ V ⋀ m ∈ ω) → ((F ∘ g):m–onto→B → B ≼ m))
119	118	19.23adv 1251	. . . . . . . . . 10 ⊢ ((F ∈ V ⋀ m ∈ ω) → (∃g(F ∘ g):m–onto→B → B ≼ m))
120		19.42v 1346	. . . . . . . . . . . . 13 ⊢ (∃g(F:A–onto→B ⋀ g:m–onto→A) ↔ (F:A–onto→B ⋀ ∃g g:m–onto→A))
121		foco 3790	. . . . . . . . . . . . . 14 ⊢ ((F:A–onto→B ⋀ g:m–onto→A) → (F ∘ g):m–onto→B)
122	121	19.22i 1076	. . . . . . . . . . . . 13 ⊢ (∃g(F:A–onto→B ⋀ g:m–onto→A) → ∃g(F ∘ g):m–onto→B)
123	120, 122	sylbir 199	. . . . . . . . . . . 12 ⊢ ((F:A–onto→B ⋀ ∃g g:m–onto→A) → ∃g(F ∘ g):m–onto→B)
124	15	bren 4518	. . . . . . . . . . . . 13 ⊢ (A ≈ m ↔ ∃f f:A–1-1-onto→m)
125		f1ocnv 3809	. . . . . . . . . . . . . . 15 ⊢ (f:A–1-1-onto→m → ◡f:m–1-1-onto→A)
126		f1ofo 3803	. . . . . . . . . . . . . . 15 ⊢ (◡f:m–1-1-onto→A → ◡f:m–onto→A)
127	63	cnvex 3625	. . . . . . . . . . . . . . . 16 ⊢ ◡f ∈ V
128		foeq1 3775	. . . . . . . . . . . . . . . 16 ⊢ (g = ◡f → (g:m–onto→A ↔ ◡f:m–onto→A))
129	127, 128	cla4ev 1915	. . . . . . . . . . . . . . 15 ⊢ (◡f:m–onto→A → ∃g g:m–onto→A)
130	125, 126, 129	3syl 20	. . . . . . . . . . . . . 14 ⊢ (f:A–1-1-onto→m → ∃g g:m–onto→A)
131	130	19.23aiv 1333	. . . . . . . . . . . . 13 ⊢ (∃f f:A–1-1-onto→m → ∃g g:m–onto→A)
132	124, 131	sylbi 197	. . . . . . . . . . . 12 ⊢ (A ≈ m → ∃g g:m–onto→A)
133	123, 132	sylan2 453	. . . . . . . . . . 11 ⊢ ((F:A–onto→B ⋀ A ≈ m) → ∃g(F ∘ g):m–onto→B)
134	133	ancoms 438	. . . . . . . . . 10 ⊢ ((A ≈ m ⋀ F:A–onto→B) → ∃g(F ∘ g):m–onto→B)
135	119, 134	syl5 21	. . . . . . . . 9 ⊢ ((F ∈ V ⋀ m ∈ ω) → ((A ≈ m ⋀ F:A–onto→B) → B ≼ m))
136	135	imp 348	. . . . . . . 8 ⊢ (((F ∈ V ⋀ m ∈ ω) ⋀ (A ≈ m ⋀ F:A–onto→B)) → B ≼ m)
137	136	anasss 442	. . . . . . 7 ⊢ ((F ∈ V ⋀ (m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B))) → B ≼ m)
138	8, 137	mpancom 709	. . . . . 6 ⊢ ((m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B)) → B ≼ m)
139	15	ensym 4553	. . . . . . 7 ⊢ (A ≈ m → m ≈ A)
140	139	ad2antrl 406	. . . . . 6 ⊢ ((m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B)) → m ≈ A)
141	1, 138, 140	sylanc 473	. . . . 5 ⊢ ((m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B)) → B ≼ A)
142	141	exp32 377	. . . 4 ⊢ (m ∈ ω → (A ≈ m → (F:A–onto→B → B ≼ A)))
143	142	r19.23aiv 1789	. . 3 ⊢ (∃m ∈ ω A ≈ m → (F:A–onto→B → B ≼ A))
144	143	imp 348	. 2 ⊢ ((∃m ∈ ω A ≈ m ⋀ F:A–onto→B) → B ≼ A)
145		isfi 4523	. 2 ⊢ (A ∈ Fin ↔ ∃m ∈ ω A ≈ m)
146	144, 145	sylanb 451	1 ⊢ ((A ∈ Fin ⋀ F:A–onto→B) → B ≼ A)

Syntax hints:   → wi 3   ⋀ wa 221  ∀wal 990   = wceq 992   ∈ wcel 994  ∃wex 1016  ∃wrex 1692  Vcvv 1857   ∪ cun 2097   ∩ cin 2098   ⊆ wss 2099  ∅c0 2332  {csn 2467   class class class wbr 2692  Ord word 2974  suc csuc 2977  ωcom 3218  ^◡ccnv 3250  dom cdm 3251   ↾ cres 3253   “ cima 3254   ∘ ccom 3255  Fun wfun 3257   Fn wfn 3258  –→wf 3259  –onto→wfo 3261  –1-1-onto→wf1o 3262   ‘cfv 3263   ≈ cen 4505   ≼ cdom 4506  Fincfn 4508

This theorem is referenced by:  fodomfib 4710  fofi 4711  iunfi 4712  pwfilem 4713  compsublem 11487  compsub 11488  hscptsscld 11491  cncomp 11494  alexsub 11500  comppfsc 11578

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-1o 4269  df-er 4401  df-en 4509  df-dom 4510  df-fin 4512

Copyright terms: Public domain