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 37584

Description: Lemma for exrecfn 37585. (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 8358	. . 3 ⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
2		peano1 7831	. . . 4 ⊢ ∅ ∈ ω
3		omelon 9555	. . . . 5 ⊢ ω ∈ On
4		limom 7824	. . . . 5 ⊢ Lim ω
5		rdglimss 37582	. . . . 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 3979	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω))
9		rdglim2a 8364	. . . . . . . 8 ⊢ ((ω ∈ On ∧ Lim ω) → (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
10	3, 4, 9	mp2an 692	. . . . . . 7 ⊢ (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢)
11	10	eleq2i 2828	. . . . . 6 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ 𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
12		eliun 4950	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
13	11, 12	bitri 275	. . . . 5 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
14		peano2 7832	. . . . . . . . 9 ⊢ (𝑢 ∈ ω → suc 𝑢 ∈ ω)
15		nnon 7814	. . . . . . . . . 10 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
16		eqid 2736	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
17	16	elrnmpt1 5909	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
18		elun2 4135	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
19	17, 18	syl 17	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
20		fvex 6847	. . . . . . . . . . . . . 14 ⊢ (rec(𝐹, 𝐴)‘𝑢) ∈ V
21		exrecfnlem.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
22		nfcv 2898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦V
23		nfcv 2898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝑧
24		nfmpt1 5197	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑧 ↦ 𝐵)
25	24	nfrn 5901	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦ran (𝑦 ∈ 𝑧 ↦ 𝐵)
26	23, 25	nfun 4122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦(𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))
27	22, 26	nfmpt 5196	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
28	21, 27	nfcxfr 2896	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐹
29		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐴
30	28, 29	nfrdg 8345	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦rec(𝐹, 𝐴)
31		nfcv 2898	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦𝑢
32	30, 31	nffv 6844	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘𝑢)
33	32	mptexgf 7168	. . . . . . . . . . . . . . . 16 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∈ V → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V)
34	20, 33	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
35	34	rnex 7852	. . . . . . . . . . . . . 14 ⊢ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
36	20, 35	unex 7689	. . . . . . . . . . . . 13 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V
37		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝐴
38		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝑢
39		nfmpt1 5197	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑧(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
40	21, 39	nfcxfr 2896	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐹
41	40, 37	nfrdg 8345	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧rec(𝐹, 𝐴)
42	41, 38	nffv 6844	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(rec(𝐹, 𝐴)‘𝑢)
43		nfcv 2898	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐵
44	42, 43	nfmpt 5196	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
45	44	nfrn 5901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
46	42, 45	nfun 4122	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
47		rdgeq1 8342	. . . . . . . . . . . . . . 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 2916	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦 𝑧 = (rec(𝐹, 𝐴)‘𝑢)
51		eqidd 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → 𝐵 = 𝐵)
52	50, 49, 51	mpteq12df 5182	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑦 ∈ 𝑧 ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
53	52	rneqd 5887	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → ran (𝑦 ∈ 𝑧 ↦ 𝐵) = ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
54	49, 53	uneq12d 4121	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
55	37, 38, 46, 48, 54	rdgsucmptf 8359	. . . . . . . . . . . . 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 2822	. . . . . . . . . . 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 37581	. . . . . . . . . 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 3135	. . . . 5 ⊢ (𝐵 ∈ 𝑊 → (∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
66	13, 65	biimtrid 242	. . . 4 ⊢ (𝐵 ∈ 𝑊 → (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
67	66	alimi 1812	. . 3 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
68		df-ral 3052	. . 3 ⊢ (∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
69	67, 68	sylibr 234	. 2 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω))
70		fvex 6847	. . 3 ⊢ (rec(𝐹, 𝐴)‘ω) ∈ V
71		sseq2 3960	. . . 4 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω)))
72		nfcv 2898	. . . . . . . 8 ⊢ Ⅎ𝑦ω
73	30, 72	nffv 6844	. . . . . . 7 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘ω)
74	73	nfeq2 2916	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = (rec(𝐹, 𝐴)‘ω)
75		eleq2 2825	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (rec(𝐹, 𝐴)‘ω)))
76		eleq2 2825	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
77	75, 76	imbi12d 344	. . . . . 6 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
78	74, 77	albid 2229	. . . . 5 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (∀𝑦(𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
79		df-ral 3052	. . . . 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 3560	. 2 ⊢ ((𝐴 ⊆ (rec(𝐹, 𝐴)‘ω) ∧ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω)) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))
83	8, 69, 82	syl2an 596	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∀wal 1539 = wceq 1541 ∃wex 1780 ∈ wcel 2113 ∀wral 3051 ∃wrex 3060 Vcvv 3440 ∪ cun 3899 ⊆ wss 3901 ∅c0 4285 ∪ ciun 4946 ↦ cmpt 5179 ran crn 5625 Oncon0 6317 Lim wlim 6318 suc csuc 6319 ‘cfv 6492 ωcom 7808 reccrdg 8340

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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pr 5377 ax-un 7680 ax-inf2 9550

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7361 df-om 7809 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341

This theorem is referenced by: exrecfn 37585

W3C validator