Theorem mnurndlem1 44882

Description: Lemma for mnurnd 44884. (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 6707	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		mnurndlem1.6	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		vex 3467	. . . . . . . 8 ⊢ 𝑖 ∈ V
5	4	prid1 4733	. . . . . . 7 ⊢ 𝑖 ∈ {𝑖, {(𝐹‘𝑖), 𝐴}}
6		simpr 489	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}})
7	5, 6	eleqtrrid 2876	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑖 ∈ 𝑣)
8		eqid 2769	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}) = (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})
9		id 23	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → 𝑖 ∈ 𝐴)
10		prex 5410	. . . . . . . 8 ⊢ {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V
11	10	a1i 11	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V)
12		id 23	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → 𝑎 = 𝑖)
13		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑎 = 𝑖 → (𝐹‘𝑎) = (𝐹‘𝑖))
14	13	preq1d 4710	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → {(𝐹‘𝑎), 𝐴} = {(𝐹‘𝑖), 𝐴})
15	12, 14	preq12d 4712	. . . . . . . 8 ⊢ (𝑎 = 𝑖 → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
16	15	adantl 486	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 = 𝑖) → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
17	8, 9, 11, 16	rr-elrnmpt3d 44823	. . . . . 6 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}))
18	7, 17	rspcime 3595	. . . . 5 ⊢ (𝑖 ∈ 𝐴 → ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣)
19	18	rgen 3087	. . . 4 ⊢ ∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣
20		ralim 3111	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
21	3, 19, 20	mpisyl 22	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
22		prex 5410	. . . . . . . 8 ⊢ {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
23	22	rgenw 3089	. . . . . . 7 ⊢ ∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
24		eleq2 2858	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 ∈ 𝑢 ↔ 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}}))
25		unieq 4887	. . . . . . . . . 10 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ∪ 𝑢 = ∪ {𝑎, {(𝐹‘𝑎), 𝐴}})
26	25	sseq1d 3976	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
27	24, 26	anbi12d 643	. . . . . . . 8 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
28	8, 27	rexrnmptw 7091	. . . . . . 7 ⊢ (∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
30		simplrl 788	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}})
31		simpr 489	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
32		mnurndlem1.4	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ∈ V
33	32	prid2 4734	. . . . . . . . . . . . . 14 ⊢ 𝐴 ∈ {(𝐹‘𝑎), 𝐴}
34		elnotel 9578	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ {(𝐹‘𝑎), 𝐴} → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
35	33, 34	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
37	31, 36	elnelneq2d 3064	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ 𝑖 = {(𝐹‘𝑎), 𝐴})
38		elpri 4618	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = 𝑎 ∨ 𝑖 = {(𝐹‘𝑎), 𝐴}))
39	38	orcomd 884	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = {(𝐹‘𝑎), 𝐴} ∨ 𝑖 = 𝑎))
40	39	ord 877	. . . . . . . . . . 11 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (¬ 𝑖 = {(𝐹‘𝑎), 𝐴} → 𝑖 = 𝑎))
41	30, 37, 40	sylc 66	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 = 𝑎)
42	41	fveq2d 6886	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) = (𝐹‘𝑎))
43		simplrr 789	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)
44		vex 3467	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
45		prex 5410	. . . . . . . . . . . . 13 ⊢ {(𝐹‘𝑎), 𝐴} ∈ V
46	44, 45	unipr 4893	. . . . . . . . . . . 12 ⊢ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} = (𝑎 ∪ {(𝐹‘𝑎), 𝐴})
47	46	sseq1i 3973	. . . . . . . . . . 11 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
48		unss 4151	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤) ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
49	48	bicomi 227	. . . . . . . . . . . 12 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 ↔ (𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤))
50	49	simprbi 502	. . . . . . . . . . 11 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
51	47, 50	sylbi 220	. . . . . . . . . 10 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
52		fvex 6895	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑎) ∈ V
53	52, 32	prss 4790	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤) ↔ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
54	53	bicomi 227	. . . . . . . . . . 11 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤))
55	54	simplbi 501	. . . . . . . . . 10 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 → (𝐹‘𝑎) ∈ 𝑤)
56	43, 51, 55	3syl 19	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑎) ∈ 𝑤)
57	42, 56	eqeltrd 2869	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) ∈ 𝑤)
58	57	ex 417	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
59	58	rexlimiva 3164	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
60	29, 59	sylbi 220	. . . . 5 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
61	60	com12 33	. . . 4 ⊢ (𝑖 ∈ 𝐴 → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝐹‘𝑖) ∈ 𝑤))
62	61	ralimia 3105	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
63	21, 62	syl 18	. 2 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
64		fnfvrnss 7117	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤) → ran 𝐹 ⊆ 𝑤)
65	2, 63, 64	syl2anc 595	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  Vcvv 3463   ∪ cun 3911   ⊆ wss 3913  {cpr 4596  ∪ cuni 4876   ↦ cmpt 5196  ran crn 5663   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-reg 9553

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-eprel 5562  df-fr 5615  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is referenced by:  mnurndlem2  44883