konigthlem

	Ref	Expression
Hypotheses	konigth.1	$⊢ A \in V$
	konigth.2	$⊢ S = ⋃_{i \in A} M (i)$
	konigth.3	$⊢ P = \underset{i \in A}{⨉} N (i)$
	konigth.4	$⊢ D = (i \in A ⟼ (a \in M (i) ⟼ f (a) (i)))$
	konigth.5	$⊢ E = (i \in A ⟼ e (i))$
Assertion	konigthlem	$⊢ \forall i \in A M (i) ≺ N (i) \to S ≺ P$

Proof

Step	Hyp	Ref	Expression
1		konigth.1	$⊢ A \in V$
2		konigth.2	$⊢ S = ⋃_{i \in A} M (i)$
3		konigth.3	$⊢ P = \underset{i \in A}{⨉} N (i)$
4		konigth.4	$⊢ D = (i \in A ⟼ (a \in M (i) ⟼ f (a) (i)))$
5		konigth.5	$⊢ E = (i \in A ⟼ e (i))$
6		fvex	$⊢ M (i) \in V$
7		fvex	$⊢ f (a) (i) \in V$
8		eqid	$⊢ (a \in M (i) ⟼ f (a) (i)) = (a \in M (i) ⟼ f (a) (i))$
9	7 8	fnmpti	$⊢ (a \in M (i) ⟼ f (a) (i)) Fn M (i)$
10	6	mptex	$⊢ (a \in M (i) ⟼ f (a) (i)) \in V$
11	4	fvmpt2	$⊢ (i \in A \land (a \in M (i) ⟼ f (a) (i)) \in V) \to D (i) = (a \in M (i) ⟼ f (a) (i))$
12	10 11	mpan2	$⊢ i \in A \to D (i) = (a \in M (i) ⟼ f (a) (i))$
13	12	fneq1d	$⊢ i \in A \to (D (i) Fn M (i) \leftrightarrow (a \in M (i) ⟼ f (a) (i)) Fn M (i))$
14	9 13	mpbiri	$⊢ i \in A \to D (i) Fn M (i)$
15		fnrndomg	$⊢ M (i) \in V \to (D (i) Fn M (i) \to ran D (i) ≼ M (i))$
16	6 14 15	mpsyl	$⊢ i \in A \to ran D (i) ≼ M (i)$
17		domsdomtr	$⊢ (ran D (i) ≼ M (i) \land M (i) ≺ N (i)) \to ran D (i) ≺ N (i)$
18	16 17	sylan	$⊢ (i \in A \land M (i) ≺ N (i)) \to ran D (i) ≺ N (i)$
19		sdomdif	$⊢ ran D (i) ≺ N (i) \to N (i) ∖ ran D (i) \neq \emptyset$
20	18 19	syl	$⊢ (i \in A \land M (i) ≺ N (i)) \to N (i) ∖ ran D (i) \neq \emptyset$
21	20	ralimiaa	$⊢ \forall i \in A M (i) ≺ N (i) \to \forall i \in A N (i) ∖ ran D (i) \neq \emptyset$
22		fvex	$⊢ N (i) \in V$
23	22	difexi	$⊢ N (i) ∖ ran D (i) \in V$
24	1 23	ac6c5	$⊢ \forall i \in A N (i) ∖ ran D (i) \neq \emptyset \to \exists e \forall i \in A e (i) \in (N (i) ∖ ran D (i))$
25		equid	$⊢ f = f$
26		eldifi	$⊢ e (i) \in (N (i) ∖ ran D (i)) \to e (i) \in N (i)$
27		fvex	$⊢ e (i) \in V$
28	5	fvmpt2	$⊢ (i \in A \land e (i) \in V) \to E (i) = e (i)$
29	27 28	mpan2	$⊢ i \in A \to E (i) = e (i)$
30	29	eleq1d	$⊢ i \in A \to (E (i) \in N (i) \leftrightarrow e (i) \in N (i))$
31	26 30	imbitrrid	$⊢ i \in A \to (e (i) \in (N (i) ∖ ran D (i)) \to E (i) \in N (i))$
32	31	ralimia	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to \forall i \in A E (i) \in N (i)$
33	27 5	fnmpti	$⊢ E Fn A$
34	32 33	jctil	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to (E Fn A \land \forall i \in A E (i) \in N (i))$
35	1	mptex	$⊢ (i \in A ⟼ e (i)) \in V$
36	5 35	eqeltri	$⊢ E \in V$
37	36	elixp	$⊢ E \in \underset{i \in A}{⨉} N (i) \leftrightarrow (E Fn A \land \forall i \in A E (i) \in N (i))$
38	34 37	sylibr	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to E \in \underset{i \in A}{⨉} N (i)$
39	38 3	eleqtrrdi	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to E \in P$
40		foelrn	$⊢ (f : S \underset{onto}{⟶} P \land E \in P) \to \exists a \in S E = f (a)$
41	40	expcom	$⊢ E \in P \to (f : S \underset{onto}{⟶} P \to \exists a \in S E = f (a))$
42	2	eleq2i	$⊢ a \in S \leftrightarrow a \in ⋃_{i \in A} M (i)$
43		eliun	$⊢ a \in ⋃_{i \in A} M (i) \leftrightarrow \exists i \in A a \in M (i)$
44	42 43	bitri	$⊢ a \in S \leftrightarrow \exists i \in A a \in M (i)$
45		nfra1	$⊢ Ⅎ i \forall i \in A e (i) \in (N (i) ∖ ran D (i))$
46		nfv	$⊢ Ⅎ i E = f (a)$
47	45 46	nfan	$⊢ Ⅎ i (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a))$
48		nfv	$⊢ Ⅎ i \neg f = f$
49	29	ad2antrl	$⊢ (E = f (a) \land (i \in A \land a \in M (i))) \to E (i) = e (i)$
50		fveq1	$⊢ E = f (a) \to E (i) = f (a) (i)$
51	12	fveq1d	$⊢ i \in A \to D (i) (a) = (a \in M (i) ⟼ f (a) (i)) (a)$
52	8	fvmpt2	$⊢ (a \in M (i) \land f (a) (i) \in V) \to (a \in M (i) ⟼ f (a) (i)) (a) = f (a) (i)$
53	7 52	mpan2	$⊢ a \in M (i) \to (a \in M (i) ⟼ f (a) (i)) (a) = f (a) (i)$
54	51 53	sylan9eq	$⊢ (i \in A \land a \in M (i)) \to D (i) (a) = f (a) (i)$
55	54	eqcomd	$⊢ (i \in A \land a \in M (i)) \to f (a) (i) = D (i) (a)$
56	50 55	sylan9eq	$⊢ (E = f (a) \land (i \in A \land a \in M (i))) \to E (i) = D (i) (a)$
57	49 56	eqtr3d	$⊢ (E = f (a) \land (i \in A \land a \in M (i))) \to e (i) = D (i) (a)$
58		fnfvelrn	$⊢ (D (i) Fn M (i) \land a \in M (i)) \to D (i) (a) \in ran D (i)$
59	14 58	sylan	$⊢ (i \in A \land a \in M (i)) \to D (i) (a) \in ran D (i)$
60	59	adantl	$⊢ (E = f (a) \land (i \in A \land a \in M (i))) \to D (i) (a) \in ran D (i)$
61	57 60	eqeltrd	$⊢ (E = f (a) \land (i \in A \land a \in M (i))) \to e (i) \in ran D (i)$
62	61	3adant1	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a) \land (i \in A \land a \in M (i))) \to e (i) \in ran D (i)$
63		simp1	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a) \land (i \in A \land a \in M (i))) \to \forall i \in A e (i) \in (N (i) ∖ ran D (i))$
64		simp3l	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a) \land (i \in A \land a \in M (i))) \to i \in A$
65		rsp	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to (i \in A \to e (i) \in (N (i) ∖ ran D (i)))$
66		eldifn	$⊢ e (i) \in (N (i) ∖ ran D (i)) \to \neg e (i) \in ran D (i)$
67	65 66	syl6	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to (i \in A \to \neg e (i) \in ran D (i))$
68	63 64 67	sylc	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a) \land (i \in A \land a \in M (i))) \to \neg e (i) \in ran D (i)$
69	62 68	pm2.21dd	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a) \land (i \in A \land a \in M (i))) \to \neg f = f$
70	69	3expia	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a)) \to ((i \in A \land a \in M (i)) \to \neg f = f)$
71	70	expd	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a)) \to (i \in A \to (a \in M (i) \to \neg f = f))$
72	47 48 71	rexlimd	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a)) \to (\exists i \in A a \in M (i) \to \neg f = f)$
73	44 72	biimtrid	$⊢ (\forall i \in A e (i) \in (N (i) ∖ ran D (i)) \land E = f (a)) \to (a \in S \to \neg f = f)$
74	73	ex	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to (E = f (a) \to (a \in S \to \neg f = f))$
75	74	com23	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to (a \in S \to (E = f (a) \to \neg f = f))$
76	75	rexlimdv	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to (\exists a \in S E = f (a) \to \neg f = f)$
77	41 76	syl9r	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to (E \in P \to (f : S \underset{onto}{⟶} P \to \neg f = f))$
78	39 77	mpd	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to (f : S \underset{onto}{⟶} P \to \neg f = f)$
79	25 78	mt2i	$⊢ \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to \neg f : S \underset{onto}{⟶} P$
80	79	exlimiv	$⊢ \exists e \forall i \in A e (i) \in (N (i) ∖ ran D (i)) \to \neg f : S \underset{onto}{⟶} P$
81	21 24 80	3syl	$⊢ \forall i \in A M (i) ≺ N (i) \to \neg f : S \underset{onto}{⟶} P$
82	81	nexdv	$⊢ \forall i \in A M (i) ≺ N (i) \to \neg \exists f f : S \underset{onto}{⟶} P$
83	6	0dom	$⊢ \emptyset ≼ M (i)$
84		domsdomtr	$⊢ (\emptyset ≼ M (i) \land M (i) ≺ N (i)) \to \emptyset ≺ N (i)$
85	83 84	mpan	$⊢ M (i) ≺ N (i) \to \emptyset ≺ N (i)$
86	22	0sdom	$⊢ \emptyset ≺ N (i) \leftrightarrow N (i) \neq \emptyset$
87	85 86	sylib	$⊢ M (i) ≺ N (i) \to N (i) \neq \emptyset$
88	87	ralimi	$⊢ \forall i \in A M (i) ≺ N (i) \to \forall i \in A N (i) \neq \emptyset$
89	3	neeq1i	$⊢ P \neq \emptyset \leftrightarrow \underset{i \in A}{⨉} N (i) \neq \emptyset$
90	22	rgenw	$⊢ \forall i \in A N (i) \in V$
91		ixpexg	$⊢ \forall i \in A N (i) \in V \to \underset{i \in A}{⨉} N (i) \in V$
92	90 91	ax-mp	$⊢ \underset{i \in A}{⨉} N (i) \in V$
93	3 92	eqeltri	$⊢ P \in V$
94	93	0sdom	$⊢ \emptyset ≺ P \leftrightarrow P \neq \emptyset$
95	1 22	ac9	$⊢ \forall i \in A N (i) \neq \emptyset \leftrightarrow \underset{i \in A}{⨉} N (i) \neq \emptyset$
96	89 94 95	3bitr4i	$⊢ \emptyset ≺ P \leftrightarrow \forall i \in A N (i) \neq \emptyset$
97	88 96	sylibr	$⊢ \forall i \in A M (i) ≺ N (i) \to \emptyset ≺ P$
98	1 6	iunex	$⊢ ⋃_{i \in A} M (i) \in V$
99	2 98	eqeltri	$⊢ S \in V$
100		domtri	$⊢ (P \in V \land S \in V) \to (P ≼ S \leftrightarrow \neg S ≺ P)$
101	93 99 100	mp2an	$⊢ P ≼ S \leftrightarrow \neg S ≺ P$
102	101	biimpri	$⊢ \neg S ≺ P \to P ≼ S$
103		fodomr	$⊢ (\emptyset ≺ P \land P ≼ S) \to \exists f f : S \underset{onto}{⟶} P$
104	97 102 103	syl2an	$⊢ (\forall i \in A M (i) ≺ N (i) \land \neg S ≺ P) \to \exists f f : S \underset{onto}{⟶} P$
105	82 104	mtand	$⊢ \forall i \in A M (i) ≺ N (i) \to \neg \neg S ≺ P$
106	105	notnotrd	$⊢ \forall i \in A M (i) ≺ N (i) \to S ≺ P$

Metamath Proof Explorer

Theorem konigthlem

Proof