Theorem mnurndlem1 40666

Description: Lemma for mnurnd 40668. (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 6515	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		mnurndlem1.6	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		vex 3497	. . . . . . . 8 ⊢ 𝑖 ∈ V
5	4	prid1 4698	. . . . . . 7 ⊢ 𝑖 ∈ {𝑖, {(𝐹‘𝑖), 𝐴}}
6		simpr 487	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}})
7	5, 6	eleqtrrid 2920	. . . . . 6 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑣 = {𝑖, {(𝐹‘𝑖), 𝐴}}) → 𝑖 ∈ 𝑣)
8		eqid 2821	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}) = (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})
9		id 22	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → 𝑖 ∈ 𝐴)
10		prex 5333	. . . . . . . 8 ⊢ {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V
11	10	a1i 11	. . . . . . 7 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ V)
12		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → 𝑎 = 𝑖)
13		fveq2 6670	. . . . . . . . . 10 ⊢ (𝑎 = 𝑖 → (𝐹‘𝑎) = (𝐹‘𝑖))
14	13	preq1d 4675	. . . . . . . . 9 ⊢ (𝑎 = 𝑖 → {(𝐹‘𝑎), 𝐴} = {(𝐹‘𝑖), 𝐴})
15	12, 14	preq12d 4677	. . . . . . . 8 ⊢ (𝑎 = 𝑖 → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
16	15	adantl 484	. . . . . . 7 ⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 = 𝑖) → {𝑎, {(𝐹‘𝑎), 𝐴}} = {𝑖, {(𝐹‘𝑖), 𝐴}})
17	8, 9, 11, 16	rr-elrnmpt3d 40610	. . . . . 6 ⊢ (𝑖 ∈ 𝐴 → {𝑖, {(𝐹‘𝑖), 𝐴}} ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}}))
18	7, 17	rspcime 3627	. . . . 5 ⊢ (𝑖 ∈ 𝐴 → ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣)
19	18	rgen 3148	. . . 4 ⊢ ∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣
20		ralim 3162	. . . 4 ⊢ (∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ 𝐴 ∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
21	3, 19, 20	mpisyl 21	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
22		prex 5333	. . . . . . . 8 ⊢ {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
23	22	rgenw 3150	. . . . . . 7 ⊢ ∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V
24		eleq2 2901	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 ∈ 𝑢 ↔ 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}}))
25		unieq 4849	. . . . . . . . . 10 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ∪ 𝑢 = ∪ {𝑎, {(𝐹‘𝑎), 𝐴}})
26	25	sseq1d 3998	. . . . . . . . 9 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
27	24, 26	anbi12d 632	. . . . . . . 8 ⊢ (𝑢 = {𝑎, {(𝐹‘𝑎), 𝐴}} → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
28	8, 27	rexrnmptw 6861	. . . . . . 7 ⊢ (∀𝑎 ∈ 𝐴 {𝑎, {(𝐹‘𝑎), 𝐴}} ∈ V → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤))
30		simplrl 775	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}})
31		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
32		mnurndlem1.4	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ∈ V
33	32	prid2 4699	. . . . . . . . . . . . . 14 ⊢ 𝐴 ∈ {(𝐹‘𝑎), 𝐴}
34		elnotel 9073	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ {(𝐹‘𝑎), 𝐴} → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
35	33, 34	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ {(𝐹‘𝑎), 𝐴} ∈ 𝐴)
37	31, 36	elnelneq2d 40605	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ¬ 𝑖 = {(𝐹‘𝑎), 𝐴})
38		elpri 4589	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = 𝑎 ∨ 𝑖 = {(𝐹‘𝑎), 𝐴}))
39	38	orcomd 867	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (𝑖 = {(𝐹‘𝑎), 𝐴} ∨ 𝑖 = 𝑎))
40	39	ord 860	. . . . . . . . . . 11 ⊢ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} → (¬ 𝑖 = {(𝐹‘𝑎), 𝐴} → 𝑖 = 𝑎))
41	30, 37, 40	sylc 65	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → 𝑖 = 𝑎)
42	41	fveq2d 6674	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) = (𝐹‘𝑎))
43		simplrr 776	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)
44		vex 3497	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
45		prex 5333	. . . . . . . . . . . . 13 ⊢ {(𝐹‘𝑎), 𝐴} ∈ V
46	44, 45	unipr 4855	. . . . . . . . . . . 12 ⊢ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} = (𝑎 ∪ {(𝐹‘𝑎), 𝐴})
47	46	sseq1i 3995	. . . . . . . . . . 11 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
48		unss 4160	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤) ↔ (𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤)
49	48	bicomi 226	. . . . . . . . . . . 12 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 ↔ (𝑎 ⊆ 𝑤 ∧ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤))
50	49	simprbi 499	. . . . . . . . . . 11 ⊢ ((𝑎 ∪ {(𝐹‘𝑎), 𝐴}) ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
51	47, 50	sylbi 219	. . . . . . . . . 10 ⊢ (∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤 → {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
52		fvex 6683	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑎) ∈ V
53	52, 32	prss 4753	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤) ↔ {(𝐹‘𝑎), 𝐴} ⊆ 𝑤)
54	53	bicomi 226	. . . . . . . . . . 11 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤))
55	54	simplbi 500	. . . . . . . . . 10 ⊢ ({(𝐹‘𝑎), 𝐴} ⊆ 𝑤 → (𝐹‘𝑎) ∈ 𝑤)
56	43, 51, 55	3syl 18	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑎) ∈ 𝑤)
57	42, 56	eqeltrd 2913	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) ∧ 𝑖 ∈ 𝐴) → (𝐹‘𝑖) ∈ 𝑤)
58	57	ex 415	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤)) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
59	58	rexlimiva 3281	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 (𝑖 ∈ {𝑎, {(𝐹‘𝑎), 𝐴}} ∧ ∪ {𝑎, {(𝐹‘𝑎), 𝐴}} ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
60	29, 59	sylbi 219	. . . . 5 ⊢ (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝑖 ∈ 𝐴 → (𝐹‘𝑖) ∈ 𝑤))
61	60	com12 32	. . . 4 ⊢ (𝑖 ∈ 𝐴 → (∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → (𝐹‘𝑖) ∈ 𝑤))
62	61	ralimia 3158	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
63	21, 62	syl 17	. 2 ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤)
64		fnfvrnss 6884	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐹‘𝑖) ∈ 𝑤) → ran 𝐹 ⊆ 𝑤)
65	2, 63, 64	syl2anc 586	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  Vcvv 3494   ∪ cun 3934   ⊆ wss 3936  {cpr 4569  ∪ cuni 4838   ↦ cmpt 5146  ran crn 5556   Fn wfn 6350  ⟶wf 6351  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-reg 9056

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-eprel 5465  df-fr 5514  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363

This theorem is referenced by:  mnurndlem2  40667