Theorem konigthlem 9993

Description: Lemma for konigth 9994. (Contributed by Mario Carneiro, 22-Feb-2013.)

Hypotheses

Ref	Expression
konigth.1	⊢ 𝐴 ∈ V
konigth.2	⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖)
konigth.3	⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖)
konigth.4	⊢ 𝐷 = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
konigth.5	⊢ 𝐸 = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖))

Assertion

Ref	Expression
konigthlem	⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃)

Distinct variable groups:   𝐴,𝑎,𝑒,𝑓,𝑖   𝐷,𝑎,𝑒   𝐸,𝑎,𝑖   𝑀,𝑎,𝑓   𝑁,𝑎,𝑒,𝑓   𝑃,𝑎,𝑒,𝑓   𝑆,𝑎,𝑒,𝑓

Allowed substitution hints:   𝐷(𝑓,𝑖)   𝑃(𝑖)   𝑆(𝑖)   𝐸(𝑒,𝑓)   𝑀(𝑒,𝑖)   𝑁(𝑖)

Proof of Theorem konigthlem

Step	Hyp	Ref	Expression
1		fvex 6686	. . . . . . . . 9 ⊢ (𝑀‘𝑖) ∈ V
2		fvex 6686	. . . . . . . . . . 11 ⊢ ((𝑓‘𝑎)‘𝑖) ∈ V
3		eqid 2824	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))
4	2, 3	fnmpti 6494	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖)
5	1	mptex 6989	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V
6		konigth.4	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
7	6	fvmpt2 6782	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V) → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
8	5, 7	mpan2 689	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
9	8	fneq1d 6449	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖) Fn (𝑀‘𝑖) ↔ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖)))
10	4, 9	mpbiri 260	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) Fn (𝑀‘𝑖))
11		fnrndomg 9961	. . . . . . . . 9 ⊢ ((𝑀‘𝑖) ∈ V → ((𝐷‘𝑖) Fn (𝑀‘𝑖) → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖)))
12	1, 10, 11	mpsyl 68	. . . . . . . 8 ⊢ (𝑖 ∈ 𝐴 → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖))
13		domsdomtr 8655	. . . . . . . 8 ⊢ ((ran (𝐷‘𝑖) ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖))
14	12, 13	sylan 582	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖))
15		sdomdif 8668	. . . . . . 7 ⊢ (ran (𝐷‘𝑖) ≺ (𝑁‘𝑖) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
16	14, 15	syl 17	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
17	16	ralimiaa 3162	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
18		konigth.1	. . . . . 6 ⊢ 𝐴 ∈ V
19		fvex 6686	. . . . . . 7 ⊢ (𝑁‘𝑖) ∈ V
20	19	difexi 5235	. . . . . 6 ⊢ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∈ V
21	18, 20	ac6c5 9907	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅ → ∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))
22		equid 2018	. . . . . . 7 ⊢ 𝑓 = 𝑓
23		eldifi 4106	. . . . . . . . . . . . 13 ⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑒‘𝑖) ∈ (𝑁‘𝑖))
24		fvex 6686	. . . . . . . . . . . . . . 15 ⊢ (𝑒‘𝑖) ∈ V
25		konigth.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖))
26	25	fvmpt2 6782	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑒‘𝑖) ∈ V) → (𝐸‘𝑖) = (𝑒‘𝑖))
27	24, 26	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ 𝐴 → (𝐸‘𝑖) = (𝑒‘𝑖))
28	27	eleq1d 2900	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → ((𝐸‘𝑖) ∈ (𝑁‘𝑖) ↔ (𝑒‘𝑖) ∈ (𝑁‘𝑖)))
29	23, 28	syl5ibr 248	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
30	29	ralimia 3161	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖))
31	24, 25	fnmpti 6494	. . . . . . . . . . 11 ⊢ 𝐸 Fn 𝐴
32	30, 31	jctil 522	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
33	18	mptex 6989	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) ∈ V
34	25, 33	eqeltri 2912	. . . . . . . . . . 11 ⊢ 𝐸 ∈ V
35	34	elixp 8471	. . . . . . . . . 10 ⊢ (𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ↔ (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
36	32, 35	sylibr 236	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖))
37		konigth.3	. . . . . . . . 9 ⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖)
38	36, 37	eleqtrrdi 2927	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ 𝑃)
39		foelrn 6875	. . . . . . . . . 10 ⊢ ((𝑓:𝑆–onto→𝑃 ∧ 𝐸 ∈ 𝑃) → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎))
40	39	expcom 416	. . . . . . . . 9 ⊢ (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎)))
41		konigth.2	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖)
42	41	eleq2i 2907	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖))
43		eliun 4926	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖))
44	42, 43	bitri 277	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑆 ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖))
45		nfra1 3222	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))
46		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖 𝐸 = (𝑓‘𝑎)
47	45, 46	nfan 1899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎))
48		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 ¬ 𝑓 = 𝑓
49	27	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = (𝑒‘𝑖))
50		fveq1 6672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐸 = (𝑓‘𝑎) → (𝐸‘𝑖) = ((𝑓‘𝑎)‘𝑖))
51	8	fveq1d 6675	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖)‘𝑎) = ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎))
52	3	fvmpt2 6782	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ∈ (𝑀‘𝑖) ∧ ((𝑓‘𝑎)‘𝑖) ∈ V) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖))
53	2, 52	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (𝑀‘𝑖) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖))
54	51, 53	sylan9eq 2879	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) = ((𝑓‘𝑎)‘𝑖))
55	54	eqcomd 2830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝑓‘𝑎)‘𝑖) = ((𝐷‘𝑖)‘𝑎))
56	50, 55	sylan9eq 2879	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = ((𝐷‘𝑖)‘𝑎))
57	49, 56	eqtr3d 2861	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) = ((𝐷‘𝑖)‘𝑎))
58		fnfvelrn 6851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐷‘𝑖) Fn (𝑀‘𝑖) ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
59	10, 58	sylan 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
60	59	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
61	57, 60	eqeltrd 2916	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
62	61	3adant1 1126	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
63		simp1 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))
64		simp3l 1197	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → 𝑖 ∈ 𝐴)
65		rsp 3208	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))))
66		eldifn 4107	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
67	65, 66	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)))
68	63, 64, 67	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
69	62, 68	pm2.21dd 197	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ¬ 𝑓 = 𝑓)
70	69	3expia 1117	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ¬ 𝑓 = 𝑓))
71	70	expd 418	. . . . . . . . . . . . . 14 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑖 ∈ 𝐴 → (𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓)))
72	47, 48, 71	rexlimd 3320	. . . . . . . . . . . . 13 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓))
73	44, 72	syl5bi 244	. . . . . . . . . . . 12 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓))
74	73	ex 415	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 = (𝑓‘𝑎) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓)))
75	74	com23 86	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑎 ∈ 𝑆 → (𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓)))
76	75	rexlimdv 3286	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓))
77	40, 76	syl9r 78	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ¬ 𝑓 = 𝑓)))
78	38, 77	mpd 15	. . . . . . 7 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑓:𝑆–onto→𝑃 → ¬ 𝑓 = 𝑓))
79	22, 78	mt2i 139	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃)
80	79	exlimiv 1930	. . . . 5 ⊢ (∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃)
81	17, 21, 80	3syl 18	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ 𝑓:𝑆–onto→𝑃)
82	81	nexdv 1936	. . 3 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ∃𝑓 𝑓:𝑆–onto→𝑃)
83	1	0dom 8650	. . . . . . . 8 ⊢ ∅ ≼ (𝑀‘𝑖)
84		domsdomtr 8655	. . . . . . . 8 ⊢ ((∅ ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ∅ ≺ (𝑁‘𝑖))
85	83, 84	mpan 688	. . . . . . 7 ⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ (𝑁‘𝑖))
86	19	0sdom 8651	. . . . . . 7 ⊢ (∅ ≺ (𝑁‘𝑖) ↔ (𝑁‘𝑖) ≠ ∅)
87	85, 86	sylib 220	. . . . . 6 ⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → (𝑁‘𝑖) ≠ ∅)
88	87	ralimi 3163	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
89	37	neeq1i 3083	. . . . . 6 ⊢ (𝑃 ≠ ∅ ↔ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
90	19	rgenw 3153	. . . . . . . . 9 ⊢ ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V
91		ixpexg 8489	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V → X𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V)
92	90, 91	ax-mp 5	. . . . . . . 8 ⊢ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V
93	37, 92	eqeltri 2912	. . . . . . 7 ⊢ 𝑃 ∈ V
94	93	0sdom 8651	. . . . . 6 ⊢ (∅ ≺ 𝑃 ↔ 𝑃 ≠ ∅)
95	18, 19	ac9 9908	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅ ↔ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
96	89, 94, 95	3bitr4i 305	. . . . 5 ⊢ (∅ ≺ 𝑃 ↔ ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
97	88, 96	sylibr 236	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ 𝑃)
98	18, 1	iunex 7672	. . . . . . 7 ⊢ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ∈ V
99	41, 98	eqeltri 2912	. . . . . 6 ⊢ 𝑆 ∈ V
100		domtri 9981	. . . . . 6 ⊢ ((𝑃 ∈ V ∧ 𝑆 ∈ V) → (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃))
101	93, 99, 100	mp2an 690	. . . . 5 ⊢ (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃)
102	101	biimpri 230	. . . 4 ⊢ (¬ 𝑆 ≺ 𝑃 → 𝑃 ≼ 𝑆)
103		fodomr 8671	. . . 4 ⊢ ((∅ ≺ 𝑃 ∧ 𝑃 ≼ 𝑆) → ∃𝑓 𝑓:𝑆–onto→𝑃)
104	97, 102, 103	syl2an 597	. . 3 ⊢ ((∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) ∧ ¬ 𝑆 ≺ 𝑃) → ∃𝑓 𝑓:𝑆–onto→𝑃)
105	82, 104	mtand 814	. 2 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ¬ 𝑆 ≺ 𝑃)
106	105	notnotrd 135	1 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1536  ∃wex 1779   ∈ wcel 2113   ≠ wne 3019  ∀wral 3141  ∃wrex 3142  Vcvv 3497   ∖ cdif 3936  ∅c0 4294  ∪ ciun 4922   class class class wbr 5069   ↦ cmpt 5149  ran crn 5559   Fn wfn 6353  –onto→wfo 6356  ‘cfv 6358  Xcixp 8464   ≼ cdom 8510   ≺ csdm 8511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-ac2 9888

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-int 4880  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-se 5518  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-isom 6367  df-riota 7117  df-ov 7162  df-oprab 7163  df-mpo 7164  df-1st 7692  df-2nd 7693  df-wrecs 7950  df-recs 8011  df-er 8292  df-map 8411  df-ixp 8465  df-en 8513  df-dom 8514  df-sdom 8515  df-card 9371  df-acn 9374  df-ac 9545

This theorem is referenced by:  konigth  9994