Theorem mnurndlem1

Description: Lemma for mnurnd . (Contributed by Rohan Ridenour, 12-Aug-2023)

	Ref	Expression
Hypotheses	mnurndlem1.3	$$⊢\phi \to F:A⟶U$$
	mnurndlem1.4	$$⊢A\in \mathrm{V}$$
	mnurndlem1.6	$$⊢\phi \to \forall i\in A\left(\exists v\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)i\in v\to \exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\right)$$
Assertion	mnurndlem1	$$⊢\phi \to \mathrm{ran}F\subseteq w$$

Proof

Step	Hyp	Ref	Expression
1		mnurndlem1.3	$$⊢\phi \to F:A⟶U$$
2		mnurndlem1.4	$$⊢A\in \mathrm{V}$$
3		mnurndlem1.6	$$⊢\phi \to \forall i\in A\left(\exists v\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)i\in v\to \exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\right)$$
4	1	ffnd	$$⊢\phi \to FFnA$$
5		vex	$$⊢i\in \mathrm{V}$$
6	5	prid1	$$⊢i\in \left\{i,\left\{F\left(i\right),A\right\}\right\}$$
7		simpr	$$⊢\left(i\in A\wedge v=\left\{i,\left\{F\left(i\right),A\right\}\right\}\right)\to v=\left\{i,\left\{F\left(i\right),A\right\}\right\}$$
8	6 7	eleqtrrid	$$⊢\left(i\in A\wedge v=\left\{i,\left\{F\left(i\right),A\right\}\right\}\right)\to i\in v$$
9		eqid	$$⊢\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)=\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)$$
10		id	$$⊢i\in A\to i\in A$$
11		prex	$$⊢\left\{i,\left\{F\left(i\right),A\right\}\right\}\in \mathrm{V}$$
12	11	a1i	$$⊢i\in A\to \left\{i,\left\{F\left(i\right),A\right\}\right\}\in \mathrm{V}$$
13		id	$$⊢a=i\to a=i$$
14		fveq2	$$⊢a=i\to F\left(a\right)=F\left(i\right)$$
15	14	preq1d	$$⊢a=i\to \left\{F\left(a\right),A\right\}=\left\{F\left(i\right),A\right\}$$
16	13 15	preq12d	$$⊢a=i\to \left\{a,\left\{F\left(a\right),A\right\}\right\}=\left\{i,\left\{F\left(i\right),A\right\}\right\}$$
17	16	adantl	$$⊢\left(i\in A\wedge a=i\right)\to \left\{a,\left\{F\left(a\right),A\right\}\right\}=\left\{i,\left\{F\left(i\right),A\right\}\right\}$$
18	9 10 12 17	rr-elrnmpt3d	$$⊢i\in A\to \left\{i,\left\{F\left(i\right),A\right\}\right\}\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)$$
19	8 18	rspcime	$$⊢i\in A\to \exists v\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)i\in v$$
20	19	rgen	$$⊢\forall i\in A\exists v\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)i\in v$$
21		ralim	$$⊢\forall i\in A\left(\exists v\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)i\in v\to \exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\right)\to \left(\forall i\in A\exists v\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)i\in v\to \forall i\in A\exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\right)$$
22	3 20 21	mpisyl	$$⊢\phi \to \forall i\in A\exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)$$
23		prex	$$⊢\left\{a,\left\{F\left(a\right),A\right\}\right\}\in \mathrm{V}$$
24	23	rgenw	$$⊢\forall a\in A\left\{a,\left\{F\left(a\right),A\right\}\right\}\in \mathrm{V}$$
25		eleq2	$$⊢u=\left\{a,\left\{F\left(a\right),A\right\}\right\}\to \left(i\in u\leftrightarrow i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\right)$$
26		unieq	$$⊢u=\left\{a,\left\{F\left(a\right),A\right\}\right\}\to \bigcup u=\bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}$$
27	26	sseq1d	$$⊢u=\left\{a,\left\{F\left(a\right),A\right\}\right\}\to \left(\bigcup u\subseteq w\leftrightarrow \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)$$
28	25 27	anbi12d	$$⊢u=\left\{a,\left\{F\left(a\right),A\right\}\right\}\to \left(\left(i\in u\wedge \bigcup u\subseteq w\right)\leftrightarrow \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)$$
29	9 28	rexrnmptw	$$⊢\forall a\in A\left\{a,\left\{F\left(a\right),A\right\}\right\}\in \mathrm{V}\to \left(\exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\leftrightarrow \exists a\in A\left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)$$
30	24 29	ax-mp	$$⊢\exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\leftrightarrow \exists a\in A\left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)$$
31		simplrl	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}$$
32		simpr	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to i\in A$$
33	2	prid2	$$⊢A\in \left\{F\left(a\right),A\right\}$$
34		elnotel	$$⊢A\in \left\{F\left(a\right),A\right\}\to \neg \left\{F\left(a\right),A\right\}\in A$$
35	33 34	ax-mp	$$⊢\neg \left\{F\left(a\right),A\right\}\in A$$
36	35	a1i	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to \neg \left\{F\left(a\right),A\right\}\in A$$
37	32 36	elnelneq2d	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to \neg i=\left\{F\left(a\right),A\right\}$$
38		elpri	$$⊢i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\to \left(i=a\vee i=\left\{F\left(a\right),A\right\}\right)$$
39	38	orcomd	$$⊢i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\to \left(i=\left\{F\left(a\right),A\right\}\vee i=a\right)$$
40	39	ord	$$⊢i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\to \left(\neg i=\left\{F\left(a\right),A\right\}\to i=a\right)$$
41	31 37 40	sylc	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to i=a$$
42	41	fveq2d	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to F\left(i\right)=F\left(a\right)$$
43		simplrr	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w$$
44		vex	$$⊢a\in \mathrm{V}$$
45		prex	$$⊢\left\{F\left(a\right),A\right\}\in \mathrm{V}$$
46	44 45	unipr	$$⊢\bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}=a\cup \left\{F\left(a\right),A\right\}$$
47	46	sseq1i	$$⊢\bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\leftrightarrow a\cup \left\{F\left(a\right),A\right\}\subseteq w$$
48		unss	$$⊢\left(a\subseteq w\wedge \left\{F\left(a\right),A\right\}\subseteq w\right)\leftrightarrow a\cup \left\{F\left(a\right),A\right\}\subseteq w$$
49	48	bicomi	$$⊢a\cup \left\{F\left(a\right),A\right\}\subseteq w\leftrightarrow \left(a\subseteq w\wedge \left\{F\left(a\right),A\right\}\subseteq w\right)$$
50	49	simprbi	$$⊢a\cup \left\{F\left(a\right),A\right\}\subseteq w\to \left\{F\left(a\right),A\right\}\subseteq w$$
51	47 50	sylbi	$$⊢\bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\to \left\{F\left(a\right),A\right\}\subseteq w$$
52		fvex	$$⊢F\left(a\right)\in \mathrm{V}$$
53	52 2	prss	$$⊢\left(F\left(a\right)\in w\wedge A\in w\right)\leftrightarrow \left\{F\left(a\right),A\right\}\subseteq w$$
54	53	bicomi	$$⊢\left\{F\left(a\right),A\right\}\subseteq w\leftrightarrow \left(F\left(a\right)\in w\wedge A\in w\right)$$
55	54	simplbi	$$⊢\left\{F\left(a\right),A\right\}\subseteq w\to F\left(a\right)\in w$$
56	43 51 55	3syl	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to F\left(a\right)\in w$$
57	42 56	eqeltrd	$$⊢\left(\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\wedge i\in A\right)\to F\left(i\right)\in w$$
58	57	ex	$$⊢\left(a\in A\wedge \left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\right)\to \left(i\in A\to F\left(i\right)\in w\right)$$
59	58	rexlimiva	$$⊢\exists a\in A\left(i\in \left\{a,\left\{F\left(a\right),A\right\}\right\}\wedge \bigcup \left\{a,\left\{F\left(a\right),A\right\}\right\}\subseteq w\right)\to \left(i\in A\to F\left(i\right)\in w\right)$$
60	30 59	sylbi	$$⊢\exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\to \left(i\in A\to F\left(i\right)\in w\right)$$
61	60	com12	$$⊢i\in A\to \left(\exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\to F\left(i\right)\in w\right)$$
62	61	ralimia	$$⊢\forall i\in A\exists u\in \mathrm{ran}\left(a\in A⟼\left\{a,\left\{F\left(a\right),A\right\}\right\}\right)\left(i\in u\wedge \bigcup u\subseteq w\right)\to \forall i\in AF\left(i\right)\in w$$
63	22 62	syl	$$⊢\phi \to \forall i\in AF\left(i\right)\in w$$
64		fnfvrnss	$$⊢\left(FFnA\wedge \forall i\in AF\left(i\right)\in w\right)\to \mathrm{ran}F\subseteq w$$
65	4 63 64	syl2anc	$$⊢\phi \to \mathrm{ran}F\subseteq w$$