Theorem mnurndlem1 43040

Description: Lemma for mnurnd 43042. (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 6719	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		mnurndlem1.6	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		vex 3479	. . . . . . . 8 ⊢ 𝑖 ∈ V
5	4	prid1 4767	. . . . . . 7 ⊢ 𝑖 ∈ {𝑖, {(𝐹‘𝑖), 𝐴}}
6		simpr 486	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}})
7	5, 6	eleqtrrid 2841	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑖 ∈ 𝑣)
8		eqid 2733	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}) = (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})
9		id 22	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → 𝑖 ∈ 𝐴)
10		prex 5433	. . . . . . . 8 ⊢ {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V
11	10	a1i 11	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V)
12		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → 𝑎 = 𝑖)
13		fveq2 6892	. . . . . . . . . 10 ⊢ (𝑎 = 𝑖 → (𝐹‘𝑎) = (𝐹‘𝑖))
14	13	preq1d 4744	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → {(𝐹‘𝑎), 𝐴} = {(𝐹‘𝑖), 𝐴})
15	12, 14	preq12d 4746	. . . . . . . 8 ⊢ (𝑎 = 𝑖 → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
16	15	adantl 483	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 = 𝑖) → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
17	8, 9, 11, 16	rr-elrnmpt3d 42960	. . . . . 6 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}))
18	7, 17	rspcime 3617	. . . . 5 ⊢ (𝑖 ∈ 𝐴 → ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣)
19	18	rgen 3064	. . . 4 ⊢ ∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣
20		ralim 3087	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
21	3, 19, 20	mpisyl 21	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
22		prex 5433	. . . . . . . 8 ⊢ {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
23	22	rgenw 3066	. . . . . . 7 ⊢ ∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
24		eleq2 2823	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 ∈ 𝑢 ↔ 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}}))
25		unieq 4920	. . . . . . . . . 10 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ∪ 𝑢 = ∪ {𝑎, {(𝐹‘𝑎), 𝐴}})
26	25	sseq1d 4014	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
27	24, 26	anbi12d 632	. . . . . . . 8 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
28	8, 27	rexrnmptw 7097	. . . . . . 7 ⊢ (∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
30		simplrl 776	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}})
31		simpr 486	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
32		mnurndlem1.4	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ∈ V
33	32	prid2 4768	. . . . . . . . . . . . . 14 ⊢ 𝐴 ∈ {(𝐹‘𝑎), 𝐴}
34		elnotel 9605	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ {(𝐹‘𝑎), 𝐴} → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
35	33, 34	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
37	31, 36	elnelneq2d 42955	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ 𝑖 = {(𝐹‘𝑎), 𝐴})
38		elpri 4651	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = 𝑎 ∨ 𝑖 = {(𝐹‘𝑎), 𝐴}))
39	38	orcomd 870	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = {(𝐹‘𝑎), 𝐴} ∨ 𝑖 = 𝑎))
40	39	ord 863	. . . . . . . . . . 11 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (¬ 𝑖 = {(𝐹‘𝑎), 𝐴} → 𝑖 = 𝑎))
41	30, 37, 40	sylc 65	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 = 𝑎)
42	41	fveq2d 6896	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) = (𝐹‘𝑎))
43		simplrr 777	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)
44		vex 3479	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
45		prex 5433	. . . . . . . . . . . . 13 ⊢ {(𝐹‘𝑎), 𝐴} ∈ V
46	44, 45	unipr 4927	. . . . . . . . . . . 12 ⊢ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} = (𝑎 ∪ {(𝐹‘𝑎), 𝐴})
47	46	sseq1i 4011	. . . . . . . . . . 11 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
48		unss 4185	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤) ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
49	48	bicomi 223	. . . . . . . . . . . 12 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 ↔ (𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤))
50	49	simprbi 498	. . . . . . . . . . 11 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
51	47, 50	sylbi 216	. . . . . . . . . 10 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
52		fvex 6905	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑎) ∈ V
53	52, 32	prss 4824	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤) ↔ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
54	53	bicomi 223	. . . . . . . . . . 11 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤))
55	54	simplbi 499	. . . . . . . . . 10 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 → (𝐹‘𝑎) ∈ 𝑤)
56	43, 51, 55	3syl 18	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑎) ∈ 𝑤)
57	42, 56	eqeltrd 2834	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) ∈ 𝑤)
58	57	ex 414	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
59	58	rexlimiva 3148	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
60	29, 59	sylbi 216	. . . . 5 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
61	60	com12 32	. . . 4 ⊢ (𝑖 ∈ 𝐴 → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝐹‘𝑖) ∈ 𝑤))
62	61	ralimia 3081	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
63	21, 62	syl 17	. 2 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
64		fnfvrnss 7120	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤) → ran 𝐹 ⊆ 𝑤)
65	2, 63, 64	syl2anc 585	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ∪ cun 3947   ⊆ wss 3949  {cpr 4631  ∪ cuni 4909   ↦ cmpt 5232  ran crn 5678   Fn wfn 6539  ⟶wf 6540  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-reg 9587

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-eprel 5581  df-fr 5632  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552

This theorem is referenced by:  mnurndlem2  43041