Theorem konigthlem 10608

Description: Lemma for konigth 10609. (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 6919	. . . . . . . . 9 ⊢ (𝑀‘𝑖) ∈ V
2		fvex 6919	. . . . . . . . . . 11 ⊢ ((𝑓‘𝑎)‘𝑖) ∈ V
3		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))
4	2, 3	fnmpti 6711	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖)
5	1	mptex 7243	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V
6		konigth.4	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
7	6	fvmpt2 7027	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V) → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
8	5, 7	mpan2 691	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
9	8	fneq1d 6661	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖) Fn (𝑀‘𝑖) ↔ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖)))
10	4, 9	mpbiri 258	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) Fn (𝑀‘𝑖))
11		fnrndomg 10576	. . . . . . . . 9 ⊢ ((𝑀‘𝑖) ∈ V → ((𝐷‘𝑖) Fn (𝑀‘𝑖) → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖)))
12	1, 10, 11	mpsyl 68	. . . . . . . 8 ⊢ (𝑖 ∈ 𝐴 → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖))
13		domsdomtr 9152	. . . . . . . 8 ⊢ ((ran (𝐷‘𝑖) ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖))
14	12, 13	sylan 580	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖))
15		sdomdif 9165	. . . . . . 7 ⊢ (ran (𝐷‘𝑖) ≺ (𝑁‘𝑖) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
16	14, 15	syl 17	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
17	16	ralimiaa 3082	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
18		konigth.1	. . . . . 6 ⊢ 𝐴 ∈ V
19		fvex 6919	. . . . . . 7 ⊢ (𝑁‘𝑖) ∈ V
20	19	difexi 5330	. . . . . 6 ⊢ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∈ V
21	18, 20	ac6c5 10522	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅ → ∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))
22		equid 2011	. . . . . . 7 ⊢ 𝑓 = 𝑓
23		eldifi 4131	. . . . . . . . . . . . 13 ⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑒‘𝑖) ∈ (𝑁‘𝑖))
24		fvex 6919	. . . . . . . . . . . . . . 15 ⊢ (𝑒‘𝑖) ∈ V
25		konigth.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖))
26	25	fvmpt2 7027	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑒‘𝑖) ∈ V) → (𝐸‘𝑖) = (𝑒‘𝑖))
27	24, 26	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ 𝐴 → (𝐸‘𝑖) = (𝑒‘𝑖))
28	27	eleq1d 2826	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → ((𝐸‘𝑖) ∈ (𝑁‘𝑖) ↔ (𝑒‘𝑖) ∈ (𝑁‘𝑖)))
29	23, 28	imbitrrid 246	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
30	29	ralimia 3080	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖))
31	24, 25	fnmpti 6711	. . . . . . . . . . 11 ⊢ 𝐸 Fn 𝐴
32	30, 31	jctil 519	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
33	18	mptex 7243	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) ∈ V
34	25, 33	eqeltri 2837	. . . . . . . . . . 11 ⊢ 𝐸 ∈ V
35	34	elixp 8944	. . . . . . . . . 10 ⊢ (𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ↔ (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
36	32, 35	sylibr 234	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖))
37		konigth.3	. . . . . . . . 9 ⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖)
38	36, 37	eleqtrrdi 2852	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ 𝑃)
39		foelrn 7127	. . . . . . . . . 10 ⊢ ((𝑓:𝑆–onto→𝑃 ∧ 𝐸 ∈ 𝑃) → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎))
40	39	expcom 413	. . . . . . . . 9 ⊢ (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎)))
41		konigth.2	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖)
42	41	eleq2i 2833	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖))
43		eliun 4995	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖))
44	42, 43	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑆 ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖))
45		nfra1 3284	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))
46		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖 𝐸 = (𝑓‘𝑎)
47	45, 46	nfan 1899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎))
48		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 ¬ 𝑓 = 𝑓
49	27	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = (𝑒‘𝑖))
50		fveq1 6905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐸 = (𝑓‘𝑎) → (𝐸‘𝑖) = ((𝑓‘𝑎)‘𝑖))
51	8	fveq1d 6908	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖)‘𝑎) = ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎))
52	3	fvmpt2 7027	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ∈ (𝑀‘𝑖) ∧ ((𝑓‘𝑎)‘𝑖) ∈ V) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖))
53	2, 52	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (𝑀‘𝑖) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖))
54	51, 53	sylan9eq 2797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) = ((𝑓‘𝑎)‘𝑖))
55	54	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝑓‘𝑎)‘𝑖) = ((𝐷‘𝑖)‘𝑎))
56	50, 55	sylan9eq 2797	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = ((𝐷‘𝑖)‘𝑎))
57	49, 56	eqtr3d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) = ((𝐷‘𝑖)‘𝑎))
58		fnfvelrn 7100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐷‘𝑖) Fn (𝑀‘𝑖) ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
59	10, 58	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
60	59	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
61	57, 60	eqeltrd 2841	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
62	61	3adant1 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
63		simp1 1137	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))
64		simp3l 1202	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → 𝑖 ∈ 𝐴)
65		rsp 3247	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))))
66		eldifn 4132	. . . . . . . . . . . . . . . . . . 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 1122	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ¬ 𝑓 = 𝑓))
71	70	expd 415	. . . . . . . . . . . . . 14 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑖 ∈ 𝐴 → (𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓)))
72	47, 48, 71	rexlimd 3266	. . . . . . . . . . . . 13 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓))
73	44, 72	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓))
74	73	ex 412	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 = (𝑓‘𝑎) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓)))
75	74	com23 86	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑎 ∈ 𝑆 → (𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓)))
76	75	rexlimdv 3153	. . . . . . . . 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 1930	. . . . 5 ⊢ (∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃)
81	17, 21, 80	3syl 18	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ 𝑓:𝑆–onto→𝑃)
82	81	nexdv 1936	. . 3 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ∃𝑓 𝑓:𝑆–onto→𝑃)
83	1	0dom 9146	. . . . . . . 8 ⊢ ∅ ≼ (𝑀‘𝑖)
84		domsdomtr 9152	. . . . . . . 8 ⊢ ((∅ ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ∅ ≺ (𝑁‘𝑖))
85	83, 84	mpan 690	. . . . . . 7 ⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ (𝑁‘𝑖))
86	19	0sdom 9147	. . . . . . 7 ⊢ (∅ ≺ (𝑁‘𝑖) ↔ (𝑁‘𝑖) ≠ ∅)
87	85, 86	sylib 218	. . . . . 6 ⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → (𝑁‘𝑖) ≠ ∅)
88	87	ralimi 3083	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
89	37	neeq1i 3005	. . . . . 6 ⊢ (𝑃 ≠ ∅ ↔ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
90	19	rgenw 3065	. . . . . . . . 9 ⊢ ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V
91		ixpexg 8962	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V → X𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V)
92	90, 91	ax-mp 5	. . . . . . . 8 ⊢ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V
93	37, 92	eqeltri 2837	. . . . . . 7 ⊢ 𝑃 ∈ V
94	93	0sdom 9147	. . . . . 6 ⊢ (∅ ≺ 𝑃 ↔ 𝑃 ≠ ∅)
95	18, 19	ac9 10523	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅ ↔ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
96	89, 94, 95	3bitr4i 303	. . . . 5 ⊢ (∅ ≺ 𝑃 ↔ ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
97	88, 96	sylibr 234	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ 𝑃)
98	18, 1	iunex 7993	. . . . . . 7 ⊢ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ∈ V
99	41, 98	eqeltri 2837	. . . . . 6 ⊢ 𝑆 ∈ V
100		domtri 10596	. . . . . 6 ⊢ ((𝑃 ∈ V ∧ 𝑆 ∈ V) → (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃))
101	93, 99, 100	mp2an 692	. . . . 5 ⊢ (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃)
102	101	biimpri 228	. . . 4 ⊢ (¬ 𝑆 ≺ 𝑃 → 𝑃 ≼ 𝑆)
103		fodomr 9168	. . . 4 ⊢ ((∅ ≺ 𝑃 ∧ 𝑃 ≼ 𝑆) → ∃𝑓 𝑓:𝑆–onto→𝑃)
104	97, 102, 103	syl2an 596	. . 3 ⊢ ((∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) ∧ ¬ 𝑆 ≺ 𝑃) → ∃𝑓 𝑓:𝑆–onto→𝑃)
105	82, 104	mtand 816	. 2 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ¬ 𝑆 ≺ 𝑃)
106	105	notnotrd 133	1 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  Vcvv 3480   ∖ cdif 3948  ∅c0 4333  ∪ ciun 4991   class class class wbr 5143   ↦ cmpt 5225  ran crn 5686   Fn wfn 6556  –onto→wfo 6559  ‘cfv 6561  Xcixp 8937   ≼ cdom 8983   ≺ csdm 8984

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-ac2 10503

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-card 9979  df-acn 9982  df-ac 10156

This theorem is referenced by:  konigth  10609