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 37870

Description: Lemma for exrecfn 37871. (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 8398	. . 3 ⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
2		peano1 7869	. . . 4 ⊢ ∅ ∈ ω
3		omelon 9601	. . . . 5 ⊢ ω ∈ On
4		limom 7862	. . . . 5 ⊢ Lim ω
5		rdglimss 37868	. . . . 5 ⊢ (((ω ∈ On ∧ Lim ω) ∧ ∅ ∈ ω) → (rec(𝐹, 𝐴)‘∅) ⊆ (rec(𝐹, 𝐴)‘ω))
6	3, 4, 5	mpanl12 712	. . . 4 ⊢ (∅ ∈ ω → (rec(𝐹, 𝐴)‘∅) ⊆ (rec(𝐹, 𝐴)‘ω))
7	2, 6	ax-mp 5	. . 3 ⊢ (rec(𝐹, 𝐴)‘∅) ⊆ (rec(𝐹, 𝐴)‘ω)
8	1, 7	eqsstrrdi 3981	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω))
9		rdglim2a 8404	. . . . . . . 8 ⊢ ((ω ∈ On ∧ Lim ω) → (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
10	3, 4, 9	mp2an 702	. . . . . . 7 ⊢ (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢)
11	10	eleq2i 2854	. . . . . 6 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ 𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
12		eliun 4953	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
13	11, 12	bitri 277	. . . . 5 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
14		peano2 7870	. . . . . . . . 9 ⊢ (𝑢 ∈ ω → suc 𝑢 ∈ ω)
15		nnon 7852	. . . . . . . . . 10 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
16		eqid 2762	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
17	16	elrnmpt1 5936	. . . . . . . . . . . 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 6880	. . . . . . . . . . . . . 14 ⊢ (rec(𝐹, 𝐴)‘𝑢) ∈ V
21		exrecfnlem.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
22		nfcv 2924	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦V
23		nfcv 2924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝑧
24		nfmpt1 5199	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑧 ↦ 𝐵)
25	24	nfrn 5928	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦ran (𝑦 ∈ 𝑧 ↦ 𝐵)
26	23, 25	nfun 4123	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦(𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))
27	22, 26	nfmpt 5198	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
28	21, 27	nfcxfr 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐹
29		nfcv 2924	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐴
30	28, 29	nfrdg 8385	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦rec(𝐹, 𝐴)
31		nfcv 2924	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦𝑢
32	30, 31	nffv 6877	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘𝑢)
33	32	mptexgf 7206	. . . . . . . . . . . . . . . 16 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∈ V → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V)
34	20, 33	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
35	34	rnex 7891	. . . . . . . . . . . . . 14 ⊢ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
36	20, 35	unex 7727	. . . . . . . . . . . . 13 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V
37		nfcv 2924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝐴
38		nfcv 2924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝑢
39		nfmpt1 5199	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑧(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
40	21, 39	nfcxfr 2922	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐹
41	40, 37	nfrdg 8385	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧rec(𝐹, 𝐴)
42	41, 38	nffv 6877	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(rec(𝐹, 𝐴)‘𝑢)
43		nfcv 2924	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐵
44	42, 43	nfmpt 5198	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
45	44	nfrn 5928	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
46	42, 45	nfun 4123	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
47		rdgeq1 8382	. . . . . . . . . . . . . . 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 2941	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦 𝑧 = (rec(𝐹, 𝐴)‘𝑢)
51		eqidd 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → 𝐵 = 𝐵)
52	50, 49, 51	mpteq12df 5184	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑦 ∈ 𝑧 ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
53	52	rneqd 5914	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → ran (𝑦 ∈ 𝑧 ↦ 𝐵) = ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
54	49, 53	uneq12d 4122	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
55	37, 38, 46, 48, 54	rdgsucmptf 8399	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ On ∧ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V) → (rec(𝐹, 𝐴)‘suc 𝑢) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
56	36, 55	mpan2 701	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ On → (rec(𝐹, 𝐴)‘suc 𝑢) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
57	56	eleq2d 2848	. . . . . . . . . . 11 ⊢ (𝑢 ∈ On → (𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) ↔ 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))))
58	19, 57	imbitrrid 248	. . . . . . . . . 10 ⊢ (𝑢 ∈ On → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢)))
59	15, 58	syl 17	. . . . . . . . 9 ⊢ (𝑢 ∈ ω → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢)))
60		rdgellim 37867	. . . . . . . . . 10 ⊢ (((ω ∈ On ∧ Lim ω) ∧ suc 𝑢 ∈ ω) → (𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
61	3, 4, 60	mpanl12 712	. . . . . . . . 9 ⊢ (suc 𝑢 ∈ ω → (𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
62	14, 59, 61	sylsyld 61	. . . . . . . 8 ⊢ (𝑢 ∈ ω → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
63	62	expd 419	. . . . . . 7 ⊢ (𝑢 ∈ ω → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → (𝐵 ∈ 𝑊 → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
64	63	com3r 87	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → (𝑢 ∈ ω → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
65	64	rexlimdv 3161	. . . . 5 ⊢ (𝐵 ∈ 𝑊 → (∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
66	13, 65	biimtrid 244	. . . 4 ⊢ (𝐵 ∈ 𝑊 → (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
67	66	alimi 1831	. . 3 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
68	67	ralrid 3084	. 2 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω))
69		fvex 6880	. . 3 ⊢ (rec(𝐹, 𝐴)‘ω) ∈ V
70		sseq2 3962	. . . 4 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω)))
71		nfcv 2924	. . . . . . . 8 ⊢ Ⅎ𝑦ω
72	30, 71	nffv 6877	. . . . . . 7 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘ω)
73	72	nfeq2 2941	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = (rec(𝐹, 𝐴)‘ω)
74		eleq2 2851	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (rec(𝐹, 𝐴)‘ω)))
75		eleq2 2851	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
76	74, 75	imbi12d 346	. . . . . 6 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
77	73, 76	albid 2257	. . . . 5 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (∀𝑦(𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
78		df-ral 3077	. . . . 5 ⊢ (∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥))
79		df-ral 3077	. . . . 5 ⊢ (∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
80	77, 78, 79	3bitr4g 316	. . . 4 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥 ↔ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
81	70, 80	anbi12d 641	. . 3 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥) ↔ (𝐴 ⊆ (rec(𝐹, 𝐴)‘ω) ∧ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
82	69, 81	spcev 3565	. 2 ⊢ ((𝐴 ⊆ (rec(𝐹, 𝐴)‘ω) ∧ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω)) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))
83	8, 68, 82	syl2an 605	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∀wal 1558 = wceq 1560 ∃wex 1799 ∈ wcel 2142 ∀wral 3076 ∃wrex 3086 Vcvv 3454 ∪ cun 3902 ⊆ wss 3904 ∅c0 4285 ∪ ciun 4949 ↦ cmpt 5181 ran crn 5648 Oncon0 6346 Lim wlim 6347 suc csuc 6348 ‘cfv 6521 ωcom 7846 reccrdg 8380

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pr 5390 ax-un 7718 ax-inf2 9596

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3077 df-rex 3087 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-ov 7399 df-om 7847 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381

This theorem is referenced by: exrecfn 37871

W3C validator