Theorem mnurndlem1 44637

Description: Lemma for mnurnd 44639. (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 6671	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		mnurndlem1.6	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		vex 3446	. . . . . . . 8 ⊢ 𝑖 ∈ V
5	4	prid1 4721	. . . . . . 7 ⊢ 𝑖 ∈ {𝑖, {(𝐹‘𝑖), 𝐴}}
6		simpr 484	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}})
7	5, 6	eleqtrrid 2844	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑖 ∈ 𝑣)
8		eqid 2737	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}) = (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})
9		id 22	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → 𝑖 ∈ 𝐴)
10		prex 5384	. . . . . . . 8 ⊢ {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V
11	10	a1i 11	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V)
12		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → 𝑎 = 𝑖)
13		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑎 = 𝑖 → (𝐹‘𝑎) = (𝐹‘𝑖))
14	13	preq1d 4698	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → {(𝐹‘𝑎), 𝐴} = {(𝐹‘𝑖), 𝐴})
15	12, 14	preq12d 4700	. . . . . . . 8 ⊢ (𝑎 = 𝑖 → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
16	15	adantl 481	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 = 𝑖) → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
17	8, 9, 11, 16	rr-elrnmpt3d 44564	. . . . . 6 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}))
18	7, 17	rspcime 3583	. . . . 5 ⊢ (𝑖 ∈ 𝐴 → ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣)
19	18	rgen 3054	. . . 4 ⊢ ∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣
20		ralim 3078	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
21	3, 19, 20	mpisyl 21	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
22		prex 5384	. . . . . . . 8 ⊢ {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
23	22	rgenw 3056	. . . . . . 7 ⊢ ∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
24		eleq2 2826	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 ∈ 𝑢 ↔ 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}}))
25		unieq 4876	. . . . . . . . . 10 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ∪ 𝑢 = ∪ {𝑎, {(𝐹‘𝑎), 𝐴}})
26	25	sseq1d 3967	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
27	24, 26	anbi12d 633	. . . . . . . 8 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
28	8, 27	rexrnmptw 7049	. . . . . . 7 ⊢ (∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
30		simplrl 777	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}})
31		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
32		mnurndlem1.4	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ∈ V
33	32	prid2 4722	. . . . . . . . . . . . . 14 ⊢ 𝐴 ∈ {(𝐹‘𝑎), 𝐴}
34		elnotel 9531	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ {(𝐹‘𝑎), 𝐴} → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
35	33, 34	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
37	31, 36	elnelneq2d 44559	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ 𝑖 = {(𝐹‘𝑎), 𝐴})
38		elpri 4606	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = 𝑎 ∨ 𝑖 = {(𝐹‘𝑎), 𝐴}))
39	38	orcomd 872	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = {(𝐹‘𝑎), 𝐴} ∨ 𝑖 = 𝑎))
40	39	ord 865	. . . . . . . . . . 11 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (¬ 𝑖 = {(𝐹‘𝑎), 𝐴} → 𝑖 = 𝑎))
41	30, 37, 40	sylc 65	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 = 𝑎)
42	41	fveq2d 6846	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) = (𝐹‘𝑎))
43		simplrr 778	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)
44		vex 3446	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
45		prex 5384	. . . . . . . . . . . . 13 ⊢ {(𝐹‘𝑎), 𝐴} ∈ V
46	44, 45	unipr 4882	. . . . . . . . . . . 12 ⊢ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} = (𝑎 ∪ {(𝐹‘𝑎), 𝐴})
47	46	sseq1i 3964	. . . . . . . . . . 11 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
48		unss 4144	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤) ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
49	48	bicomi 224	. . . . . . . . . . . 12 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 ↔ (𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤))
50	49	simprbi 497	. . . . . . . . . . 11 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
51	47, 50	sylbi 217	. . . . . . . . . 10 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
52		fvex 6855	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑎) ∈ V
53	52, 32	prss 4778	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤) ↔ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
54	53	bicomi 224	. . . . . . . . . . 11 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤))
55	54	simplbi 496	. . . . . . . . . 10 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 → (𝐹‘𝑎) ∈ 𝑤)
56	43, 51, 55	3syl 18	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑎) ∈ 𝑤)
57	42, 56	eqeltrd 2837	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) ∈ 𝑤)
58	57	ex 412	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
59	58	rexlimiva 3131	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
60	29, 59	sylbi 217	. . . . 5 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
61	60	com12 32	. . . 4 ⊢ (𝑖 ∈ 𝐴 → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝐹‘𝑖) ∈ 𝑤))
62	61	ralimia 3072	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
63	21, 62	syl 17	. 2 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
64		fnfvrnss 7075	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤) → ran 𝐹 ⊆ 𝑤)
65	2, 63, 64	syl2anc 585	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  Vcvv 3442   ∪ cun 3901   ⊆ wss 3903  {cpr 4584  ∪ cuni 4865   ↦ cmpt 5181  ran crn 5633   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500

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-sep 5243  ax-nul 5253  ax-pr 5379  ax-reg 9509

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  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-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-eprel 5532  df-fr 5585  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-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508

This theorem is referenced by:  mnurndlem2  44638