Theorem mnurndlem1 45051

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

Hypotheses

Ref	Expression
mnurndlem1.3	⊢ (𝜑 → 𝐹:𝐴⟶𝑈)
mnurndlem1.4	⊢ 𝐴 ∈ V
mnurndlem1.6	⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))

Assertion

Ref	Expression
mnurndlem1	⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)

Distinct variable groups:   𝑣,𝐹   𝑤,𝑢,𝑖,𝑎   𝑣,𝐴,𝑖,𝑎   𝑢,𝐴   𝑢,𝐹,𝑖,𝑎

Allowed substitution hints:   𝜑(𝑤, 𝑣, 𝑢, 𝑖, 𝑎)   𝐴(𝑤)   𝑈(𝑤, 𝑣, 𝑢, 𝑖, 𝑎)   𝐹(𝑤)

Proof of Theorem mnurndlem1

Step	Hyp	Ref	Expression
1		mnurndlem1.3	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝑈)
2	1	ffnd 6710	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		mnurndlem1.6	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		vex 3461	. . . . . . . 8 ⊢ 𝑖 ∈ V
5	4	prid1 4730	. . . . . . 7 ⊢ 𝑖 ∈ {𝑖, {(𝐹‘𝑖), 𝐴}}
6		simpr 490	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}})
7	5, 6	eleqtrrid 2872	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑖 ∈ 𝑣)
8		eqid 2765	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}) = (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})
9		id 23	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → 𝑖 ∈ 𝐴)
10		prex 5411	. . . . . . . 8 ⊢ {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V
11	10	a1i 11	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V)
12		id 23	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → 𝑎 = 𝑖)
13		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑎 = 𝑖 → (𝐹‘𝑎) = (𝐹‘𝑖))
14	13	preq1d 4707	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → {(𝐹‘𝑎), 𝐴} = {(𝐹‘𝑖), 𝐴})
15	12, 14	preq12d 4709	. . . . . . . 8 ⊢ (𝑎 = 𝑖 → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
16	15	adantl 487	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 = 𝑖) → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
17	8, 9, 11, 16	rr-elrnmpt3d 44992	. . . . . 6 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}))
18	7, 17	rspcime 3588	. . . . 5 ⊢ (𝑖 ∈ 𝐴 → ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣)
19	18	rgen 3083	. . . 4 ⊢ ∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣
20		ralim 3107	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
21	3, 19, 20	mpisyl 22	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
22		prex 5411	. . . . . . . 8 ⊢ {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
23	22	rgenw 3085	. . . . . . 7 ⊢ ∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
24		eleq2 2854	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 ∈ 𝑢 ↔ 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}}))
25		unieq 4885	. . . . . . . . . 10 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ∪ 𝑢 = ∪ {𝑎, {(𝐹‘𝑎), 𝐴}})
26	25	sseq1d 3969	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
27	24, 26	anbi12d 644	. . . . . . . 8 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
28	8, 27	rexrnmptw 7094	. . . . . . 7 ⊢ (∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
30		simplrl 789	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}})
31		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
32		mnurndlem1.4	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ∈ V
33	32	prid2 4731	. . . . . . . . . . . . . 14 ⊢ 𝐴 ∈ {(𝐹‘𝑎), 𝐴}
34		elnotel 9586	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ {(𝐹‘𝑎), 𝐴} → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
35	33, 34	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
37	31, 36	elnelneq2d 3060	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ 𝑖 = {(𝐹‘𝑎), 𝐴})
38		elpri 4615	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = 𝑎 ∨ 𝑖 = {(𝐹‘𝑎), 𝐴}))
39	38	orcomd 885	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = {(𝐹‘𝑎), 𝐴} ∨ 𝑖 = 𝑎))
40	39	ord 878	. . . . . . . . . . 11 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (¬ 𝑖 = {(𝐹‘𝑎), 𝐴} → 𝑖 = 𝑎))
41	30, 37, 40	sylc 66	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 = 𝑎)
42	41	fveq2d 6889	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) = (𝐹‘𝑎))
43		simplrr 790	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)
44		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
45		prex 5411	. . . . . . . . . . . . 13 ⊢ {(𝐹‘𝑎), 𝐴} ∈ V
46	44, 45	unipr 4891	. . . . . . . . . . . 12 ⊢ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} = (𝑎 ∪ {(𝐹‘𝑎), 𝐴})
47	46	sseq1i 3966	. . . . . . . . . . 11 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
48		unss 4143	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤) ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
49	48	bicomi 227	. . . . . . . . . . . 12 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 ↔ (𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤))
50	49	simprbi 503	. . . . . . . . . . 11 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
51	47, 50	sylbi 220	. . . . . . . . . 10 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
52		fvex 6898	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑎) ∈ V
53	52, 32	prss 4788	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤) ↔ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
54	53	bicomi 227	. . . . . . . . . . 11 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤))
55	54	simplbi 502	. . . . . . . . . 10 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 → (𝐹‘𝑎) ∈ 𝑤)
56	43, 51, 55	3syl 19	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑎) ∈ 𝑤)
57	42, 56	eqeltrd 2865	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) ∈ 𝑤)
58	57	ex 418	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
59	58	rexlimiva 3160	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
60	29, 59	sylbi 220	. . . . 5 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
61	60	com12 33	. . . 4 ⊢ (𝑖 ∈ 𝐴 → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝐹‘𝑖) ∈ 𝑤))
62	61	ralimia 3101	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
63	21, 62	syl 18	. 2 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
64		fnfvrnss 7120	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤) → ran 𝐹 ⊆ 𝑤)
65	2, 63, 64	syl2anc 596	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091  Vcvv 3457   ∪ cun 3904   ⊆ wss 3906  {cpr 4593  ∪ cuni 4874   ↦ cmpt 5194  ran crn 5664   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-reg 9561

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-eprel 5563  df-fr 5616  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548

This theorem is used by:  mnurndlem2  45052