Theorem konigthlem 10491

Description: Lemma for konigth 10492. (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 6855	. . . . . . . . 9 ⊢ (𝑀‘𝑖) ∈ V
2		fvex 6855	. . . . . . . . . . 11 ⊢ ((𝑓‘𝑎)‘𝑖) ∈ V
3		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))
4	2, 3	fnmpti 6643	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖)
5	1	mptex 7179	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V
6		konigth.4	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
7	6	fvmpt2 6961	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V) → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
8	5, 7	mpan2 692	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))
9	8	fneq1d 6593	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖) Fn (𝑀‘𝑖) ↔ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖)))
10	4, 9	mpbiri 258	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) Fn (𝑀‘𝑖))
11		fnrndomg 10458	. . . . . . . . 9 ⊢ ((𝑀‘𝑖) ∈ V → ((𝐷‘𝑖) Fn (𝑀‘𝑖) → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖)))
12	1, 10, 11	mpsyl 68	. . . . . . . 8 ⊢ (𝑖 ∈ 𝐴 → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖))
13		domsdomtr 9052	. . . . . . . 8 ⊢ ((ran (𝐷‘𝑖) ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖))
14	12, 13	sylan 581	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖))
15		sdomdif 9065	. . . . . . 7 ⊢ (ran (𝐷‘𝑖) ≺ (𝑁‘𝑖) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
16	14, 15	syl 17	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
17	16	ralimiaa 3074	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅)
18		konigth.1	. . . . . 6 ⊢ 𝐴 ∈ V
19		fvex 6855	. . . . . . 7 ⊢ (𝑁‘𝑖) ∈ V
20	19	difexi 5277	. . . . . 6 ⊢ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∈ V
21	18, 20	ac6c5 10404	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅ → ∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))
22		equid 2014	. . . . . . 7 ⊢ 𝑓 = 𝑓
23		eldifi 4085	. . . . . . . . . . . . 13 ⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑒‘𝑖) ∈ (𝑁‘𝑖))
24		fvex 6855	. . . . . . . . . . . . . . 15 ⊢ (𝑒‘𝑖) ∈ V
25		konigth.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖))
26	25	fvmpt2 6961	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑒‘𝑖) ∈ V) → (𝐸‘𝑖) = (𝑒‘𝑖))
27	24, 26	mpan2 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ 𝐴 → (𝐸‘𝑖) = (𝑒‘𝑖))
28	27	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → ((𝐸‘𝑖) ∈ (𝑁‘𝑖) ↔ (𝑒‘𝑖) ∈ (𝑁‘𝑖)))
29	23, 28	imbitrrid 246	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
30	29	ralimia 3072	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖))
31	24, 25	fnmpti 6643	. . . . . . . . . . 11 ⊢ 𝐸 Fn 𝐴
32	30, 31	jctil 519	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
33	18	mptex 7179	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) ∈ V
34	25, 33	eqeltri 2833	. . . . . . . . . . 11 ⊢ 𝐸 ∈ V
35	34	elixp 8854	. . . . . . . . . 10 ⊢ (𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ↔ (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)))
36	32, 35	sylibr 234	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖))
37		konigth.3	. . . . . . . . 9 ⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖)
38	36, 37	eleqtrrdi 2848	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ 𝑃)
39		foelrn 7061	. . . . . . . . . 10 ⊢ ((𝑓:𝑆–onto→𝑃 ∧ 𝐸 ∈ 𝑃) → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎))
40	39	expcom 413	. . . . . . . . 9 ⊢ (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎)))
41		konigth.2	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖)
42	41	eleq2i 2829	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖))
43		eliun 4952	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖))
44	42, 43	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑆 ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖))
45		nfra1 3262	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))
46		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖 𝐸 = (𝑓‘𝑎)
47	45, 46	nfan 1901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎))
48		nfv 1916	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 ¬ 𝑓 = 𝑓
49	27	ad2antrl 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = (𝑒‘𝑖))
50		fveq1 6841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐸 = (𝑓‘𝑎) → (𝐸‘𝑖) = ((𝑓‘𝑎)‘𝑖))
51	8	fveq1d 6844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖)‘𝑎) = ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎))
52	3	fvmpt2 6961	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ∈ (𝑀‘𝑖) ∧ ((𝑓‘𝑎)‘𝑖) ∈ V) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖))
53	2, 52	mpan2 692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (𝑀‘𝑖) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖))
54	51, 53	sylan9eq 2792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) = ((𝑓‘𝑎)‘𝑖))
55	54	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝑓‘𝑎)‘𝑖) = ((𝐷‘𝑖)‘𝑎))
56	50, 55	sylan9eq 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = ((𝐷‘𝑖)‘𝑎))
57	49, 56	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) = ((𝐷‘𝑖)‘𝑎))
58		fnfvelrn 7034	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐷‘𝑖) Fn (𝑀‘𝑖) ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
59	10, 58	sylan 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
60	59	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖))
61	57, 60	eqeltrd 2837	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
62	61	3adant1 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))
63		simp1 1137	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))
64		simp3l 1203	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → 𝑖 ∈ 𝐴)
65		rsp 3226	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))))
66		eldifn 4086	. . . . . . . . . . . . . . . . . . 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 3245	. . . . . . . . . . . . 13 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓))
73	44, 72	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓))
74	73	ex 412	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 = (𝑓‘𝑎) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓)))
75	74	com23 86	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑎 ∈ 𝑆 → (𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓)))
76	75	rexlimdv 3137	. . . . . . . . 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 1932	. . . . 5 ⊢ (∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃)
81	17, 21, 80	3syl 18	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ 𝑓:𝑆–onto→𝑃)
82	81	nexdv 1938	. . 3 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ∃𝑓 𝑓:𝑆–onto→𝑃)
83	1	0dom 9047	. . . . . . . 8 ⊢ ∅ ≼ (𝑀‘𝑖)
84		domsdomtr 9052	. . . . . . . 8 ⊢ ((∅ ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ∅ ≺ (𝑁‘𝑖))
85	83, 84	mpan 691	. . . . . . 7 ⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ (𝑁‘𝑖))
86	19	0sdom 9048	. . . . . . 7 ⊢ (∅ ≺ (𝑁‘𝑖) ↔ (𝑁‘𝑖) ≠ ∅)
87	85, 86	sylib 218	. . . . . 6 ⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → (𝑁‘𝑖) ≠ ∅)
88	87	ralimi 3075	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
89	37	neeq1i 2997	. . . . . 6 ⊢ (𝑃 ≠ ∅ ↔ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
90	19	rgenw 3056	. . . . . . . . 9 ⊢ ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V
91		ixpexg 8872	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V → X𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V)
92	90, 91	ax-mp 5	. . . . . . . 8 ⊢ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ∈ V
93	37, 92	eqeltri 2833	. . . . . . 7 ⊢ 𝑃 ∈ V
94	93	0sdom 9048	. . . . . 6 ⊢ (∅ ≺ 𝑃 ↔ 𝑃 ≠ ∅)
95	18, 19	ac9 10405	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅ ↔ X𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
96	89, 94, 95	3bitr4i 303	. . . . 5 ⊢ (∅ ≺ 𝑃 ↔ ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅)
97	88, 96	sylibr 234	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ 𝑃)
98	18, 1	iunex 7922	. . . . . . 7 ⊢ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ∈ V
99	41, 98	eqeltri 2833	. . . . . 6 ⊢ 𝑆 ∈ V
100		domtri 10478	. . . . . 6 ⊢ ((𝑃 ∈ V ∧ 𝑆 ∈ V) → (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃))
101	93, 99, 100	mp2an 693	. . . . 5 ⊢ (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃)
102	101	biimpri 228	. . . 4 ⊢ (¬ 𝑆 ≺ 𝑃 → 𝑃 ≼ 𝑆)
103		fodomr 9068	. . . 4 ⊢ ((∅ ≺ 𝑃 ∧ 𝑃 ≼ 𝑆) → ∃𝑓 𝑓:𝑆–onto→𝑃)
104	97, 102, 103	syl2an 597	. . 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 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3442   ∖ cdif 3900  ∅c0 4287  ∪ ciun 4948   class class class wbr 5100   ↦ cmpt 5181  ran crn 5633   Fn wfn 6495  –onto→wfo 6498  ‘cfv 6500  Xcixp 8847   ≼ cdom 8893   ≺ csdm 8894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-ac2 10385

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-er 8645  df-map 8777  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-card 9863  df-acn 9866  df-ac 10038

This theorem is referenced by:  konigth  10492