Theorem konigthlem 10459

Description: Lemma for konigth 10460. (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 6835	. . . . . . . . 9 ⊢ (𝑀‘𝑖) ∈ V
2		fvex 6835	. . . . . . . . . . 11 ⊢ ((𝑓‘𝑎)‘𝑖) ∈ V
3		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))
4	2, 3	fnmpti 6624	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖)
5	1	mptex 7157	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V
6		konigth.4	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
7	6	fvmpt2 6940	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V) → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
8	5, 7	mpan2 691	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
9	8	fneq1d 6574	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖) Fn (𝑀‘𝑖) ↔ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖)))
10	4, 9	mpbiri 258	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) Fn (𝑀‘𝑖))
11		fnrndomg 10427	. . . . . . . . 9 ⊢ ((𝑀‘𝑖) ∈ V → ((𝐷‘𝑖) Fn (𝑀‘𝑖) → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖)))
12	1, 10, 11	mpsyl 68	. . . . . . . 8 ⊢ (𝑖 ∈ 𝐴 → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖))
13		domsdomtr 9025	. . . . . . . 8 ⊢ ((ran (𝐷‘𝑖) ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖))
14	12, 13	sylan 580	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖))
15		sdomdif 9038	. . . . . . 7 ⊢ (ran (𝐷‘𝑖) ≺ (𝑁‘𝑖) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
16	14, 15	syl 17	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
17	16	ralimiaa 3068	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
18		konigth.1	. . . . . 6 ⊢ 𝐴 ∈ V
19		fvex 6835	. . . . . . 7 ⊢ (𝑁‘𝑖) ∈ V
20	19	difexi 5268	. . . . . 6 ⊢ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∈ V
21	18, 20	ac6c5 10373	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅ → ∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))
22		equid 2013	. . . . . . 7 ⊢ 𝑓 = 𝑓
23		eldifi 4081	. . . . . . . . . . . . 13 ⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑒‘𝑖) ∈ (𝑁‘𝑖))
24		fvex 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑒‘𝑖) ∈ V
25		konigth.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖))
26	25	fvmpt2 6940	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑒‘𝑖) ∈ V) → (𝐸‘𝑖) = (𝑒‘𝑖))
27	24, 26	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ 𝐴 → (𝐸‘𝑖) = (𝑒‘𝑖))
28	27	eleq1d 2816	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → ((𝐸‘𝑖) ∈ (𝑁‘𝑖) ↔ (𝑒‘𝑖) ∈ (𝑁‘𝑖)))
29	23, 28	imbitrrid 246	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
30	29	ralimia 3066	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖))
31	24, 25	fnmpti 6624	. . . . . . . . . . 11 ⊢ 𝐸 Fn 𝐴
32	30, 31	jctil 519	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
33	18	mptex 7157	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) ∈ V
34	25, 33	eqeltri 2827	. . . . . . . . . . 11 ⊢ 𝐸 ∈ V
35	34	elixp 8828	. . . . . . . . . 10 ⊢ (𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ↔ (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
36	32, 35	sylibr 234	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖))
37		konigth.3	. . . . . . . . 9 ⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖)
38	36, 37	eleqtrrdi 2842	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ 𝑃)
39		foelrn 7040	. . . . . . . . . 10 ⊢ ((𝑓:𝑆–onto→𝑃 ∧ 𝐸 ∈ 𝑃) → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎))
40	39	expcom 413	. . . . . . . . 9 ⊢ (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎)))
41		konigth.2	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖)
42	41	eleq2i 2823	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖))
43		eliun 4945	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖))
44	42, 43	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑆 ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖))
45		nfra1 3256	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))
46		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖 𝐸 = (𝑓‘𝑎)
47	45, 46	nfan 1900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎))
48		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 ¬ 𝑓 = 𝑓
49	27	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = (𝑒‘𝑖))
50		fveq1 6821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐸 = (𝑓‘𝑎) → (𝐸‘𝑖) = ((𝑓‘𝑎)‘𝑖))
51	8	fveq1d 6824	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖)‘𝑎) = ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎))
52	3	fvmpt2 6940	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ∈ (𝑀‘𝑖) ∧ ((𝑓‘𝑎)‘𝑖) ∈ V) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖))
53	2, 52	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (𝑀‘𝑖) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖))
54	51, 53	sylan9eq 2786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) = ((𝑓‘𝑎)‘𝑖))
55	54	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝑓‘𝑎)‘𝑖) = ((𝐷‘𝑖)‘𝑎))
56	50, 55	sylan9eq 2786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = ((𝐷‘𝑖)‘𝑎))
57	49, 56	eqtr3d 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) = ((𝐷‘𝑖)‘𝑎))
58		fnfvelrn 7013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐷‘𝑖) Fn (𝑀‘𝑖) ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
59	10, 58	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
60	59	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
61	57, 60	eqeltrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
62	61	3adant1 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
63		simp1 1136	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))
64		simp3l 1202	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → 𝑖 ∈ 𝐴)
65		rsp 3220	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))))
66		eldifn 4082	. . . . . . . . . . . . . . . . . . 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 195	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ¬ 𝑓 = 𝑓)
70	69	3expia 1121	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ¬ 𝑓 = 𝑓))
71	70	expd 415	. . . . . . . . . . . . . 14 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑖 ∈ 𝐴 → (𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓)))
72	47, 48, 71	rexlimd 3239	. . . . . . . . . . . . 13 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓))
73	44, 72	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓))
74	73	ex 412	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 = (𝑓‘𝑎) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓)))
75	74	com23 86	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑎 ∈ 𝑆 → (𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓)))
76	75	rexlimdv 3131	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓))
77	40, 76	syl9r 78	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ¬ 𝑓 = 𝑓)))
78	38, 77	mpd 15	. . . . . . 7 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑓:𝑆–onto→𝑃 → ¬ 𝑓 = 𝑓))
79	22, 78	mt2i 137	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃)
80	79	exlimiv 1931	. . . . 5 ⊢ (∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃)
81	17, 21, 80	3syl 18	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ 𝑓:𝑆–onto→𝑃)
82	81	nexdv 1937	. . 3 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ∃𝑓 𝑓:𝑆–onto→𝑃)
83	1	0dom 9020	. . . . . . . 8 ⊢ ∅ ≼ (𝑀‘𝑖)
84		domsdomtr 9025	. . . . . . . 8 ⊢ ((∅ ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ∅ ≺ (𝑁‘𝑖))
85	83, 84	mpan 690	. . . . . . 7 ⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ (𝑁‘𝑖))
86	19	0sdom 9021	. . . . . . 7 ⊢ (∅ ≺ (𝑁‘𝑖) ↔ (𝑁‘𝑖) ≠ ∅)
87	85, 86	sylib 218	. . . . . 6 ⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → (𝑁‘𝑖) ≠ ∅)
88	87	ralimi 3069	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
89	37	neeq1i 2992	. . . . . 6 ⊢ (𝑃 ≠ ∅ ↔ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
90	19	rgenw 3051	. . . . . . . . 9 ⊢ ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V
91		ixpexg 8846	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V → X𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V)
92	90, 91	ax-mp 5	. . . . . . . 8 ⊢ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V
93	37, 92	eqeltri 2827	. . . . . . 7 ⊢ 𝑃 ∈ V
94	93	0sdom 9021	. . . . . 6 ⊢ (∅ ≺ 𝑃 ↔ 𝑃 ≠ ∅)
95	18, 19	ac9 10374	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅ ↔ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
96	89, 94, 95	3bitr4i 303	. . . . 5 ⊢ (∅ ≺ 𝑃 ↔ ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
97	88, 96	sylibr 234	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ 𝑃)
98	18, 1	iunex 7900	. . . . . . 7 ⊢ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ∈ V
99	41, 98	eqeltri 2827	. . . . . 6 ⊢ 𝑆 ∈ V
100		domtri 10447	. . . . . 6 ⊢ ((𝑃 ∈ V ∧ 𝑆 ∈ V) → (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃))
101	93, 99, 100	mp2an 692	. . . . 5 ⊢ (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃)
102	101	biimpri 228	. . . 4 ⊢ (¬ 𝑆 ≺ 𝑃 → 𝑃 ≼ 𝑆)
103		fodomr 9041	. . . 4 ⊢ ((∅ ≺ 𝑃 ∧ 𝑃 ≼ 𝑆) → ∃𝑓 𝑓:𝑆–onto→𝑃)
104	97, 102, 103	syl2an 596	. . 3 ⊢ ((∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) ∧ ¬ 𝑆 ≺ 𝑃) → ∃𝑓 𝑓:𝑆–onto→𝑃)
105	82, 104	mtand 815	. 2 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ¬ 𝑆 ≺ 𝑃)
106	105	notnotrd 133	1 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ∖ cdif 3899  ∅c0 4283  ∪ ciun 4941   class class class wbr 5091   ↦ cmpt 5172  ran crn 5617   Fn wfn 6476  –onto→wfo 6479  ‘cfv 6481  Xcixp 8821   ≼ cdom 8867   ≺ csdm 8868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-ac2 10354

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-int 4898  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-se 5570  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-isom 6490  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-er 8622  df-map 8752  df-ixp 8822  df-en 8870  df-dom 8871  df-sdom 8872  df-card 9832  df-acn 9835  df-ac 10007

This theorem is referenced by:  konigth  10460