exrecfnlem - Mathbox for ML

	Mathbox for ML		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > exrecfnlem		Structured version Visualization version GIF version

Theorem exrecfnlem 37367

Description: Lemma for exrecfn 37368. (Contributed by ML, 30-Mar-2022.)

**Hypothesis**
Ref	Expression
exrecfnlem.1	⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))

**Assertion**
Ref	Expression
exrecfnlem	⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))

Distinct variable groups: 𝑦,𝐴,𝑧,𝑥 𝑥,𝐵,𝑧 𝑥,𝐹 𝑦,𝑊 Allowed substitution hints: 𝐵(𝑦) 𝐹(𝑦,𝑧) 𝑉(𝑥,𝑦,𝑧) 𝑊(𝑥,𝑧)

Proof of Theorem exrecfnlem Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rdg0g 8395	. . 3 ⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
2		peano1 7865	. . . 4 ⊢ ∅ ∈ ω
3		omelon 9599	. . . . 5 ⊢ ω ∈ On
4		limom 7858	. . . . 5 ⊢ Lim ω
5		rdglimss 37365	. . . . 5 ⊢ (((ω ∈ On ∧ Lim ω) ∧ ∅ ∈ ω) → (rec(𝐹, 𝐴)‘∅) ⊆ (rec(𝐹, 𝐴)‘ω))
6	3, 4, 5	mpanl12 702	. . . 4 ⊢ (∅ ∈ ω → (rec(𝐹, 𝐴)‘∅) ⊆ (rec(𝐹, 𝐴)‘ω))
7	2, 6	ax-mp 5	. . 3 ⊢ (rec(𝐹, 𝐴)‘∅) ⊆ (rec(𝐹, 𝐴)‘ω)
8	1, 7	eqsstrrdi 3992	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω))
9		rdglim2a 8401	. . . . . . . 8 ⊢ ((ω ∈ On ∧ Lim ω) → (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
10	3, 4, 9	mp2an 692	. . . . . . 7 ⊢ (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢)
11	10	eleq2i 2820	. . . . . 6 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ 𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
12		eliun 4959	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
13	11, 12	bitri 275	. . . . 5 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
14		peano2 7866	. . . . . . . . 9 ⊢ (𝑢 ∈ ω → suc 𝑢 ∈ ω)
15		nnon 7848	. . . . . . . . . 10 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
16		eqid 2729	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
17	16	elrnmpt1 5924	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
18		elun2 4146	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
19	17, 18	syl 17	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
20		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (rec(𝐹, 𝐴)‘𝑢) ∈ V
21		exrecfnlem.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
22		nfcv 2891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦V
23		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝑧
24		nfmpt1 5206	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑧 ↦ 𝐵)
25	24	nfrn 5916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦ran (𝑦 ∈ 𝑧 ↦ 𝐵)
26	23, 25	nfun 4133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦(𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))
27	22, 26	nfmpt 5205	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
28	21, 27	nfcxfr 2889	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐹
29		nfcv 2891	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐴
30	28, 29	nfrdg 8382	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦rec(𝐹, 𝐴)
31		nfcv 2891	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦𝑢
32	30, 31	nffv 6868	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘𝑢)
33	32	mptexgf 7196	. . . . . . . . . . . . . . . 16 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∈ V → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V)
34	20, 33	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
35	34	rnex 7886	. . . . . . . . . . . . . 14 ⊢ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
36	20, 35	unex 7720	. . . . . . . . . . . . 13 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V
37		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝐴
38		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝑢
39		nfmpt1 5206	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑧(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
40	21, 39	nfcxfr 2889	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐹
41	40, 37	nfrdg 8382	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧rec(𝐹, 𝐴)
42	41, 38	nffv 6868	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(rec(𝐹, 𝐴)‘𝑢)
43		nfcv 2891	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐵
44	42, 43	nfmpt 5205	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
45	44	nfrn 5916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
46	42, 45	nfun 4133	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
47		rdgeq1 8379	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))) → rec(𝐹, 𝐴) = rec((𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))), 𝐴))
48	21, 47	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ rec(𝐹, 𝐴) = rec((𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))), 𝐴)
49		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → 𝑧 = (rec(𝐹, 𝐴)‘𝑢))
50	32	nfeq2 2909	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦 𝑧 = (rec(𝐹, 𝐴)‘𝑢)
51		eqidd 2730	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → 𝐵 = 𝐵)
52	50, 49, 51	mpteq12df 5191	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑦 ∈ 𝑧 ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
53	52	rneqd 5902	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → ran (𝑦 ∈ 𝑧 ↦ 𝐵) = ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
54	49, 53	uneq12d 4132	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
55	37, 38, 46, 48, 54	rdgsucmptf 8396	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ On ∧ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V) → (rec(𝐹, 𝐴)‘suc 𝑢) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
56	36, 55	mpan2 691	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ On → (rec(𝐹, 𝐴)‘suc 𝑢) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
57	56	eleq2d 2814	. . . . . . . . . . 11 ⊢ (𝑢 ∈ On → (𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) ↔ 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))))
58	19, 57	imbitrrid 246	. . . . . . . . . 10 ⊢ (𝑢 ∈ On → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢)))
59	15, 58	syl 17	. . . . . . . . 9 ⊢ (𝑢 ∈ ω → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢)))
60		rdgellim 37364	. . . . . . . . . 10 ⊢ (((ω ∈ On ∧ Lim ω) ∧ suc 𝑢 ∈ ω) → (𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
61	3, 4, 60	mpanl12 702	. . . . . . . . 9 ⊢ (suc 𝑢 ∈ ω → (𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
62	14, 59, 61	sylsyld 61	. . . . . . . 8 ⊢ (𝑢 ∈ ω → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
63	62	expd 415	. . . . . . 7 ⊢ (𝑢 ∈ ω → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → (𝐵 ∈ 𝑊 → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
64	63	com3r 87	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → (𝑢 ∈ ω → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
65	64	rexlimdv 3132	. . . . 5 ⊢ (𝐵 ∈ 𝑊 → (∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
66	13, 65	biimtrid 242	. . . 4 ⊢ (𝐵 ∈ 𝑊 → (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
67	66	alimi 1811	. . 3 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
68		df-ral 3045	. . 3 ⊢ (∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
69	67, 68	sylibr 234	. 2 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω))
70		fvex 6871	. . 3 ⊢ (rec(𝐹, 𝐴)‘ω) ∈ V
71		sseq2 3973	. . . 4 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω)))
72		nfcv 2891	. . . . . . . 8 ⊢ Ⅎ𝑦ω
73	30, 72	nffv 6868	. . . . . . 7 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘ω)
74	73	nfeq2 2909	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = (rec(𝐹, 𝐴)‘ω)
75		eleq2 2817	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (rec(𝐹, 𝐴)‘ω)))
76		eleq2 2817	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
77	75, 76	imbi12d 344	. . . . . 6 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
78	74, 77	albid 2223	. . . . 5 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (∀𝑦(𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
79		df-ral 3045	. . . . 5 ⊢ (∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥))
80	78, 79, 68	3bitr4g 314	. . . 4 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥 ↔ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
81	71, 80	anbi12d 632	. . 3 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥) ↔ (𝐴 ⊆ (rec(𝐹, 𝐴)‘ω) ∧ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
82	70, 81	spcev 3572	. 2 ⊢ ((𝐴 ⊆ (rec(𝐹, 𝐴)‘ω) ∧ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω)) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))
83	8, 69, 82	syl2an 596	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3447 ∪ cun 3912 ⊆ wss 3914 ∅c0 4296 ∪ ciun 4955 ↦ cmpt 5188 ran crn 5639 Oncon0 6332 Lim wlim 6333 suc csuc 6334 ‘cfv 6511 ωcom 7842 reccrdg 8377

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pr 5387 ax-un 7711 ax-inf2 9594

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-ov 7390 df-om 7843 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378

This theorem is referenced by: exrecfn 37368

W3C validator