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 37397

Description: Lemma for exrecfn 37398. (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 8441	. . 3 ⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
2		peano1 7884	. . . 4 ⊢ ∅ ∈ ω
3		omelon 9660	. . . . 5 ⊢ ω ∈ On
4		limom 7877	. . . . 5 ⊢ Lim ω
5		rdglimss 37395	. . . . 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 4004	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω))
9		rdglim2a 8447	. . . . . . . 8 ⊢ ((ω ∈ On ∧ Lim ω) → (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
10	3, 4, 9	mp2an 692	. . . . . . 7 ⊢ (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢)
11	10	eleq2i 2826	. . . . . 6 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ 𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
12		eliun 4971	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
13	11, 12	bitri 275	. . . . 5 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
14		peano2 7886	. . . . . . . . 9 ⊢ (𝑢 ∈ ω → suc 𝑢 ∈ ω)
15		nnon 7867	. . . . . . . . . 10 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
16		eqid 2735	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
17	16	elrnmpt1 5940	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
18		elun2 4158	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
19	17, 18	syl 17	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
20		fvex 6889	. . . . . . . . . . . . . 14 ⊢ (rec(𝐹, 𝐴)‘𝑢) ∈ V
21		exrecfnlem.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
22		nfcv 2898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦V
23		nfcv 2898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝑧
24		nfmpt1 5220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑧 ↦ 𝐵)
25	24	nfrn 5932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦ran (𝑦 ∈ 𝑧 ↦ 𝐵)
26	23, 25	nfun 4145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦(𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))
27	22, 26	nfmpt 5219	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
28	21, 27	nfcxfr 2896	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐹
29		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐴
30	28, 29	nfrdg 8428	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦rec(𝐹, 𝐴)
31		nfcv 2898	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦𝑢
32	30, 31	nffv 6886	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘𝑢)
33	32	mptexgf 7214	. . . . . . . . . . . . . . . 16 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∈ V → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V)
34	20, 33	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
35	34	rnex 7906	. . . . . . . . . . . . . 14 ⊢ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
36	20, 35	unex 7738	. . . . . . . . . . . . 13 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V
37		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝐴
38		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝑢
39		nfmpt1 5220	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑧(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
40	21, 39	nfcxfr 2896	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐹
41	40, 37	nfrdg 8428	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧rec(𝐹, 𝐴)
42	41, 38	nffv 6886	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(rec(𝐹, 𝐴)‘𝑢)
43		nfcv 2898	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐵
44	42, 43	nfmpt 5219	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
45	44	nfrn 5932	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
46	42, 45	nfun 4145	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
47		rdgeq1 8425	. . . . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → 𝐵 = 𝐵)
52	50, 49, 51	mpteq12df 5204	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑦 ∈ 𝑧 ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
53	52	rneqd 5918	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → ran (𝑦 ∈ 𝑧 ↦ 𝐵) = ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
54	49, 53	uneq12d 4144	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
55	37, 38, 46, 48, 54	rdgsucmptf 8442	. . . . . . . . . . . . 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 2820	. . . . . . . . . . 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 37394	. . . . . . . . . 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 3139	. . . . 5 ⊢ (𝐵 ∈ 𝑊 → (∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
66	13, 65	biimtrid 242	. . . 4 ⊢ (𝐵 ∈ 𝑊 → (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
67	66	alimi 1811	. . 3 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
68		df-ral 3052	. . 3 ⊢ (∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
69	67, 68	sylibr 234	. 2 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω))
70		fvex 6889	. . 3 ⊢ (rec(𝐹, 𝐴)‘ω) ∈ V
71		sseq2 3985	. . . 4 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω)))
72		nfcv 2898	. . . . . . . 8 ⊢ Ⅎ𝑦ω
73	30, 72	nffv 6886	. . . . . . 7 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘ω)
74	73	nfeq2 2916	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = (rec(𝐹, 𝐴)‘ω)
75		eleq2 2823	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (rec(𝐹, 𝐴)‘ω)))
76		eleq2 2823	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
77	75, 76	imbi12d 344	. . . . . 6 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
78	74, 77	albid 2222	. . . . 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 3585	. 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 2108 ∀wral 3051 ∃wrex 3060 Vcvv 3459 ∪ cun 3924 ⊆ wss 3926 ∅c0 4308 ∪ ciun 4967 ↦ cmpt 5201 ran crn 5655 Oncon0 6352 Lim wlim 6353 suc csuc 6354 ‘cfv 6531 ωcom 7861 reccrdg 8423

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pr 5402 ax-un 7729 ax-inf2 9655

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 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7408 df-om 7862 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424

This theorem is referenced by: exrecfn 37398

W3C validator