Theorem fodomfi 4546

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

Assertion

Ref	Expression
fodomfi	⊢ ((∃n ∈ ω A ≈ n ⋀ F:A–onto→B) → B ≼ A)

Distinct variable group:   A,n

Proof of Theorem fodomfi

Step	Hyp	Ref	Expression
1		domentr 4408	. . . . . 6 ⊢ ((B ≼ m ⋀ m ≈ A) → B ≼ A)
2		fex 3643	. . . . . . . . . 10 ⊢ ((F:A–→B ⋀ A ∈ V) → F ∈ V)
3	2	ancoms 436	. . . . . . . . 9 ⊢ ((A ∈ V ⋀ F:A–→B) → F ∈ V)
4		relen 4360	. . . . . . . . . 10 ⊢ Rel ≈
5	4	brrelexi 3203	. . . . . . . . 9 ⊢ (A ≈ m → A ∈ V)
6		fof 3663	. . . . . . . . 9 ⊢ (F:A–onto→B → F:A–→B)
7	3, 5, 6	syl2an 454	. . . . . . . 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 1809	. . . . . . . . . . . . . 14 ⊢ g ∈ V
10		coexg 3516	. . . . . . . . . . . . . 14 ⊢ ((F ∈ V ⋀ g ∈ V) → (F ∘ g) ∈ V)
11	9, 10	mpan2 695	. . . . . . . . . . . . 13 ⊢ (F ∈ V → (F ∘ g) ∈ V)
12		foeq1 3659	. . . . . . . . . . . . . 14 ⊢ (f = (F ∘ g) → (f:m–onto→B ↔ (F ∘ g):m–onto→B))
13	12	cla4egv 1859	. . . . . . . . . . . . 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 1809	. . . . . . . . . . . . . . . 16 ⊢ m ∈ V
16		fornex 3670	. . . . . . . . . . . . . . . 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 1293	. . . . . . . . . . . . . 14 ⊢ (∃f f:m–onto→B → B ∈ V)
19		foeq3 3661	. . . . . . . . . . . . . . . . . 18 ⊢ (x = B → (f:m–onto→x ↔ f:m–onto→B))
20	19	exbidv 1277	. . . . . . . . . . . . . . . . 17 ⊢ (x = B → (∃f f:m–onto→x ↔ ∃f f:m–onto→B))
21		breq1 2617	. . . . . . . . . . . . . . . . 17 ⊢ (x = B → (x ≼ m ↔ B ≼ m))
22	20, 21	imbi12d 625	. . . . . . . . . . . . . . . 16 ⊢ (x = B → ((∃f f:m–onto→x → x ≼ m) ↔ (∃f f:m–onto→B → B ≼ m)))
23	22	cla4gv 1858	. . . . . . . . . . . . . . 15 ⊢ (B ∈ V → (∀x(∃f f:m–onto→x → x ≼ m) → (∃f f:m–onto→B → B ≼ m)))
24		foeq2 3660	. . . . . . . . . . . . . . . . . . 19 ⊢ (m = ∅ → (f:m–onto→x ↔ f:∅–onto→x))
25	24	exbidv 1277	. . . . . . . . . . . . . . . . . 18 ⊢ (m = ∅ → (∃f f:m–onto→x ↔ ∃f f:∅–onto→x))
26		breq2 2618	. . . . . . . . . . . . . . . . . 18 ⊢ (m = ∅ → (x ≼ m ↔ x ≼ ∅))
27	25, 26	imbi12d 625	. . . . . . . . . . . . . . . . 17 ⊢ (m = ∅ → ((∃f f:m–onto→x → x ≼ m) ↔ (∃f f:∅–onto→x → x ≼ ∅)))
28	27	albidv 1276	. . . . . . . . . . . . . . . 16 ⊢ (m = ∅ → (∀x(∃f f:m–onto→x → x ≼ m) ↔ ∀x(∃f f:∅–onto→x → x ≼ ∅)))
29		foeq2 3660	. . . . . . . . . . . . . . . . . . 19 ⊢ (m = k → (f:m–onto→x ↔ f:k–onto→x))
30	29	exbidv 1277	. . . . . . . . . . . . . . . . . 18 ⊢ (m = k → (∃f f:m–onto→x ↔ ∃f f:k–onto→x))
31		breq2 2618	. . . . . . . . . . . . . . . . . 18 ⊢ (m = k → (x ≼ m ↔ x ≼ k))
32	30, 31	imbi12d 625	. . . . . . . . . . . . . . . . 17 ⊢ (m = k → ((∃f f:m–onto→x → x ≼ m) ↔ (∃f f:k–onto→x → x ≼ k)))
33	32	albidv 1276	. . . . . . . . . . . . . . . 16 ⊢ (m = k → (∀x(∃f f:m–onto→x → x ≼ m) ↔ ∀x(∃f f:k–onto→x → x ≼ k)))
34		foeq2 3660	. . . . . . . . . . . . . . . . . . 19 ⊢ (m = suc k → (f:m–onto→x ↔ f:suc k–onto→x))
35	34	exbidv 1277	. . . . . . . . . . . . . . . . . 18 ⊢ (m = suc k → (∃f f:m–onto→x ↔ ∃f f:suc k–onto→x))
36		breq2 2618	. . . . . . . . . . . . . . . . . 18 ⊢ (m = suc k → (x ≼ m ↔ x ≼ suc k))
37	35, 36	imbi12d 625	. . . . . . . . . . . . . . . . 17 ⊢ (m = suc k → ((∃f f:m–onto→x → x ≼ m) ↔ (∃f f:suc k–onto→x → x ≼ suc k)))
38	37	albidv 1276	. . . . . . . . . . . . . . . 16 ⊢ (m = suc k → (∀x(∃f f:m–onto→x → x ≼ m) ↔ ∀x(∃f f:suc k–onto→x → x ≼ suc k)))
39		fo00 3706	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f:∅–onto→x ↔ (f = ∅ ⋀ x = ∅))
40	39	pm3.27bi 326	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:∅–onto→x → x = ∅)
41		0dom 4450	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ≼ ∅
42	40, 41	syl6eqbr 2647	. . . . . . . . . . . . . . . . . 18 ⊢ (f:∅–onto→x → x ≼ ∅)
43	42	19.23aiv 1293	. . . . . . . . . . . . . . . . 17 ⊢ (∃f f:∅–onto→x → x ≼ ∅)
44	43	ax-gen 961	. . . . . . . . . . . . . . . 16 ⊢ ∀x(∃f f:∅–onto→x → x ≼ ∅)
45		fof 3663	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc k–onto→x → f:suc k–→x)
46		ffn 3619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc k–→x → f Fn suc k)
47		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ k ∈ V
48	47	sucid 3046	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ k ∈ suc k
49		fnsnfv 3758	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f Fn suc k ⋀ k ∈ suc k) → {(f ‘k)} = (f “ {k}))
50	48, 49	mpan2 695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f Fn suc k → {(f ‘k)} = (f “ {k}))
51	45, 46, 50	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc k–onto→x → {(f ‘k)} = (f “ {k}))
52	51	uneq2d 2180	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc k–onto→x → ((f “ k) ∪ {(f ‘k)}) = ((f “ k) ∪ (f “ {k})))
53		foima 3667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc k–onto→x → (f “ suc k) = x)
54		df-suc 2949	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ suc k = (k ∪ {k})
55		imaeq2 3394	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (suc k = (k ∪ {k}) → (f “ suc k) = (f “ (k ∪ {k})))
56	54, 55	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f “ suc k) = (f “ (k ∪ {k}))
57		imaun 3452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f “ (k ∪ {k})) = ((f “ k) ∪ (f “ {k}))
58	56, 57	eqtr2 1493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f “ k) ∪ (f “ {k})) = (f “ suc k)
59	53, 58	syl5eq 1516	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc k–onto→x → ((f “ k) ∪ (f “ {k})) = x)
60	52, 59	eqtrd 1504	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc k–onto→x → ((f “ k) ∪ {(f ‘k)}) = x)
61	60	adantl 388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → ((f “ k) ∪ {(f ‘k)}) = x)
62		snex 2745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {(f ‘k)} ∈ V
63		snex 2745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {k} ∈ V
64	47, 62, 63	undom 4424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((f “ k) ≼ k ⋀ {(f ‘k)} ≼ {k}) ⋀ (k ∩ {k}) = ∅) → ((f “ k) ∪ {(f ‘k)}) ≼ (k ∪ {k}))
65		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ f ∈ V
66		imaexg 3408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f ∈ V → (f “ k) ∈ V)
67	65, 66	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f “ k) ∈ V
68		foeq3 3661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (y = (f “ k) → (g:k–onto→y ↔ g:k–onto→(f “ k)))
69	68	exbidv 1277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (y = (f “ k) → (∃g g:k–onto→y ↔ ∃g g:k–onto→(f “ k)))
70		breq1 2617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (y = (f “ k) → (y ≼ k ↔ (f “ k) ≼ k))
71	69, 70	imbi12d 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (y = (f “ k) → ((∃g g:k–onto→y → y ≼ k) ↔ (∃g g:k–onto→(f “ k) → (f “ k) ≼ k)))
72	67, 71	cla4v 1864	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀y(∃g g:k–onto→y → y ≼ k) → (∃g g:k–onto→(f “ k) → (f “ k) ≼ k))
73	72	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀y(∃g g:k–onto→y → y ≼ k) ⋀ ∃g g:k–onto→(f “ k)) → (f “ k) ≼ k)
74		fores 3672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Fun f ⋀ k ⊆ dom f) → (f ↾ k):k–onto→(f “ k))
75		fofun 3664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f:suc k–onto→x → Fun f)
76		sssucid 3042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ k ⊆ suc k
77		fdm 3623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f:suc k–→x → dom f = suc k)
78	77	sseq2d 2085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (f:suc k–→x → (k ⊆ dom f ↔ k ⊆ suc k))
79	76, 78	mpbiri 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f:suc k–→x → k ⊆ dom f)
80	45, 79	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f:suc k–onto→x → k ⊆ dom f)
81	74, 75, 80	sylanc 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (f:suc k–onto→x → (f ↾ k):k–onto→(f “ k))
82		resexg 3386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f ∈ V → (f ↾ k) ∈ V)
83	65, 82	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f ↾ k) ∈ V
84		foeq1 3659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (g = (f ↾ k) → (g:k–onto→(f “ k) ↔ (f ↾ k):k–onto→(f “ k)))
85	83, 84	cla4ev 1865	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f ↾ k):k–onto→(f “ k) → ∃g g:k–onto→(f “ k))
86	81, 85	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:suc k–onto→x → ∃g g:k–onto→(f “ k))
87	73, 86	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀y(∃g g:k–onto→y → y ≼ k) ⋀ f:suc k–onto→x) → (f “ k) ≼ k)
88	87	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → (f “ k) ≼ k)
89		fvex 3723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f ‘k) ∈ V
90		en2sn 4418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((f ‘k) ∈ V ⋀ k ∈ V) → {(f ‘k)} ≈ {k})
91	89, 47, 90	mp2an 696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {(f ‘k)} ≈ {k}
92		endom 4372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({(f ‘k)} ≈ {k} → {(f ‘k)} ≼ {k})
93	91, 92	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {(f ‘k)} ≼ {k}
94	88, 93	jctir 293	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → ((f “ k) ≼ k ⋀ {(f ‘k)} ≼ {k}))
95		nnord 3135	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (k ∈ ω → Ord k)
96		orddisj 2980	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord k → (k ∩ {k}) = ∅)
97	95, 96	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (k ∈ ω → (k ∩ {k}) = ∅)
98	97	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → (k ∩ {k}) = ∅)
99	64, 94, 98	sylanc 471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → ((f “ k) ∪ {(f ‘k)}) ≼ (k ∪ {k}))
100	61, 99	eqbrtrrd 2632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → x ≼ (k ∪ {k}))
101	100, 54	syl6breqr 2650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) ⋀ f:suc k–onto→x) → x ≼ suc k)
102	101	ex 373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) → (f:suc k–onto→x → x ≼ suc k))
103	102	19.23adv 1212	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ω ⋀ ∀y(∃g g:k–onto→y → y ≼ k)) → (∃f f:suc k–onto→x → x ≼ suc k))
104	103	ex 373	. . . . . . . . . . . . . . . . . 18 ⊢ (k ∈ ω → (∀y(∃g g:k–onto→y → y ≼ k) → (∃f f:suc k–onto→x → x ≼ suc k)))
105	104	19.21adv 1286	. . . . . . . . . . . . . . . . 17 ⊢ (k ∈ ω → (∀y(∃g g:k–onto→y → y ≼ k) → ∀x(∃f f:suc k–onto→x → x ≼ suc k)))
106		foeq3 3661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = y → (f:k–onto→x ↔ f:k–onto→y))
107	106	exbidv 1277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = y → (∃f f:k–onto→x ↔ ∃f f:k–onto→y))
108		foeq1 3659	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f = g → (f:k–onto→y ↔ g:k–onto→y))
109	108	cbvexv 1313	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃f f:k–onto→y ↔ ∃g g:k–onto→y)
110	107, 109	syl6bb 535	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → (∃f f:k–onto→x ↔ ∃g g:k–onto→y))
111		breq1 2617	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → (x ≼ k ↔ y ≼ k))
112	110, 111	imbi12d 625	. . . . . . . . . . . . . . . . . 18 ⊢ (x = y → ((∃f f:k–onto→x → x ≼ k) ↔ (∃g g:k–onto→y → y ≼ k)))
113	112	cbvalv 1312	. . . . . . . . . . . . . . . . 17 ⊢ (∀x(∃f f:k–onto→x → x ≼ k) ↔ ∀y(∃g g:k–onto→y → y ≼ k))
114	105, 113	syl5ib 206	. . . . . . . . . . . . . . . 16 ⊢ (k ∈ ω → (∀x(∃f f:k–onto→x → x ≼ k) → ∀x(∃f f:suc k–onto→x → x ≼ suc k)))
115	28, 33, 38, 44, 114	finds1 3154	. . . . . . . . . . . . . . 15 ⊢ (m ∈ ω → ∀x(∃f f:m–onto→x → x ≼ m))
116	23, 115	syl5 21	. . . . . . . . . . . . . 14 ⊢ (B ∈ V → (m ∈ ω → (∃f f:m–onto→B → B ≼ m)))
117	18, 116	syl 10	. . . . . . . . . . . . 13 ⊢ (∃f f:m–onto→B → (m ∈ ω → (∃f f:m–onto→B → B ≼ m)))
118	117	pm2.43b 67	. . . . . . . . . . . 12 ⊢ (m ∈ ω → (∃f f:m–onto→B → B ≼ m))
119	14, 118	sylan9 468	. . . . . . . . . . 11 ⊢ ((F ∈ V ⋀ m ∈ ω) → ((F ∘ g):m–onto→B → B ≼ m))
120	119	19.23adv 1212	. . . . . . . . . 10 ⊢ ((F ∈ V ⋀ m ∈ ω) → (∃g(F ∘ g):m–onto→B → B ≼ m))
121		19.42v 1306	. . . . . . . . . . . . 13 ⊢ (∃g(F:A–onto→B ⋀ g:m–onto→A) ↔ (F:A–onto→B ⋀ ∃g g:m–onto→A))
122		foco 3673	. . . . . . . . . . . . . 14 ⊢ ((F:A–onto→B ⋀ g:m–onto→A) → (F ∘ g):m–onto→B)
123	122	19.22i 1038	. . . . . . . . . . . . 13 ⊢ (∃g(F:A–onto→B ⋀ g:m–onto→A) → ∃g(F ∘ g):m–onto→B)
124	121, 123	sylbir 201	. . . . . . . . . . . 12 ⊢ ((F:A–onto→B ⋀ ∃g g:m–onto→A) → ∃g(F ∘ g):m–onto→B)
125	15	bren 4365	. . . . . . . . . . . . 13 ⊢ (A ≈ m ↔ ∃f f:A–1-1-onto→m)
126		f1ocnv 3692	. . . . . . . . . . . . . . 15 ⊢ (f:A–1-1-onto→m → ◡f:m–1-1-onto→A)
127		f1ofo 3686	. . . . . . . . . . . . . . 15 ⊢ (◡f:m–1-1-onto→A → ◡f:m–onto→A)
128	65	cnvex 3512	. . . . . . . . . . . . . . . 16 ⊢ ◡f ∈ V
129		foeq1 3659	. . . . . . . . . . . . . . . 16 ⊢ (g = ◡f → (g:m–onto→A ↔ ◡f:m–onto→A))
130	128, 129	cla4ev 1865	. . . . . . . . . . . . . . 15 ⊢ (◡f:m–onto→A → ∃g g:m–onto→A)
131	126, 127, 130	3syl 20	. . . . . . . . . . . . . 14 ⊢ (f:A–1-1-onto→m → ∃g g:m–onto→A)
132	131	19.23aiv 1293	. . . . . . . . . . . . 13 ⊢ (∃f f:A–1-1-onto→m → ∃g g:m–onto→A)
133	125, 132	sylbi 199	. . . . . . . . . . . 12 ⊢ (A ≈ m → ∃g g:m–onto→A)
134	124, 133	sylan2 451	. . . . . . . . . . 11 ⊢ ((F:A–onto→B ⋀ A ≈ m) → ∃g(F ∘ g):m–onto→B)
135	134	ancoms 436	. . . . . . . . . 10 ⊢ ((A ≈ m ⋀ F:A–onto→B) → ∃g(F ∘ g):m–onto→B)
136	120, 135	syl5 21	. . . . . . . . 9 ⊢ ((F ∈ V ⋀ m ∈ ω) → ((A ≈ m ⋀ F:A–onto→B) → B ≼ m))
137	136	imp 350	. . . . . . . 8 ⊢ (((F ∈ V ⋀ m ∈ ω) ⋀ (A ≈ m ⋀ F:A–onto→B)) → B ≼ m)
138	137	anasss 440	. . . . . . 7 ⊢ ((F ∈ V ⋀ (m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B))) → B ≼ m)
139	8, 138	mpancom 704	. . . . . 6 ⊢ ((m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B)) → B ≼ m)
140	15	ensym 4399	. . . . . . 7 ⊢ (A ≈ m → m ≈ A)
141	140	ad2antrl 406	. . . . . 6 ⊢ ((m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B)) → m ≈ A)
142	1, 139, 141	sylanc 471	. . . . 5 ⊢ ((m ∈ ω ⋀ (A ≈ m ⋀ F:A–onto→B)) → B ≼ A)
143	142	exp32 377	. . . 4 ⊢ (m ∈ ω → (A ≈ m → (F:A–onto→B → B ≼ A)))
144	143	r19.23aiv 1740	. . 3 ⊢ (∃m ∈ ω A ≈ m → (F:A–onto→B → B ≼ A))
145	144	imp 350	. 2 ⊢ ((∃m ∈ ω A ≈ m ⋀ F:A–onto→B) → B ≼ A)
146		breq2 2618	. . 3 ⊢ (n = m → (A ≈ n ↔ A ≈ m))
147	146	cbvrexv 1797	. 2 ⊢ (∃n ∈ ω A ≈ n ↔ ∃m ∈ ω A ≈ m)
148	145, 147	sylanb 449	1 ⊢ ((∃n ∈ ω A ≈ n ⋀ F:A–onto→B) → B ≼ A)

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  ∃wrex 1643  Vcvv 1807   ∪ cun 2041   ∩ cin 2042   ⊆ wss 2043  ∅c0 2276  {csn 2405   class class class wbr 2614  Ord word 2942  suc csuc 2945  ωcom 3126  ^◡ccnv 3164  dom cdm 3165   ↾ cres 3167   “ cima 3168   ∘ ccom 3169  Fun wfun 3171   Fn wfn 3172  –→wf 3173  –onto→wfo 3175  –1-1-onto→wf1o 3176   ‘cfv 3177   ≈ cen 4354   ≼ cdom 4355

This theorem is referenced by:  fodomfib 4547  fofi 4548  iunfi 4549  pwfilem 4550

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-f1 3190  df-fo 3191  df-f1o 3192  df-fv 3193  df-1o 4123  df-er 4251  df-en 4357  df-dom 4358

Copyright terms: Public domain