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 37374

Description: Lemma for exrecfn 37375. (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 7868	. . . 4 ⊢ ∅ ∈ ω
3		omelon 9606	. . . . 5 ⊢ ω ∈ On
4		limom 7861	. . . . 5 ⊢ Lim ω
5		rdglimss 37372	. . . . 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 3995	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω))
9		rdglim2a 8404	. . . . . . . 8 ⊢ ((ω ∈ On ∧ Lim ω) → (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
10	3, 4, 9	mp2an 692	. . . . . . 7 ⊢ (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢)
11	10	eleq2i 2821	. . . . . 6 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ 𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢))
12		eliun 4962	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
13	11, 12	bitri 275	. . . . 5 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢))
14		peano2 7869	. . . . . . . . 9 ⊢ (𝑢 ∈ ω → suc 𝑢 ∈ ω)
15		nnon 7851	. . . . . . . . . 10 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
16		eqid 2730	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
17	16	elrnmpt1 5927	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
18		elun2 4149	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
19	17, 18	syl 17	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
20		fvex 6874	. . . . . . . . . . . . . 14 ⊢ (rec(𝐹, 𝐴)‘𝑢) ∈ V
21		exrecfnlem.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
22		nfcv 2892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦V
23		nfcv 2892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝑧
24		nfmpt1 5209	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑧 ↦ 𝐵)
25	24	nfrn 5919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦ran (𝑦 ∈ 𝑧 ↦ 𝐵)
26	23, 25	nfun 4136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦(𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))
27	22, 26	nfmpt 5208	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
28	21, 27	nfcxfr 2890	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐹
29		nfcv 2892	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦𝐴
30	28, 29	nfrdg 8385	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦rec(𝐹, 𝐴)
31		nfcv 2892	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦𝑢
32	30, 31	nffv 6871	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘𝑢)
33	32	mptexgf 7199	. . . . . . . . . . . . . . . 16 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∈ V → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V)
34	20, 33	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
35	34	rnex 7889	. . . . . . . . . . . . . 14 ⊢ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V
36	20, 35	unex 7723	. . . . . . . . . . . . 13 ⊢ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V
37		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝐴
38		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝑢
39		nfmpt1 5209	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑧(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))
40	21, 39	nfcxfr 2890	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐹
41	40, 37	nfrdg 8385	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧rec(𝐹, 𝐴)
42	41, 38	nffv 6871	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(rec(𝐹, 𝐴)‘𝑢)
43		nfcv 2892	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧𝐵
44	42, 43	nfmpt 5208	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
45	44	nfrn 5919	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)
46	42, 45	nfun 4136	. . . . . . . . . . . . . 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 2910	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦 𝑧 = (rec(𝐹, 𝐴)‘𝑢)
51		eqidd 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → 𝐵 = 𝐵)
52	50, 49, 51	mpteq12df 5194	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑦 ∈ 𝑧 ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
53	52	rneqd 5905	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → ran (𝑦 ∈ 𝑧 ↦ 𝐵) = ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))
54	49, 53	uneq12d 4135	. . . . . . . . . . . . . 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 691	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ On → (rec(𝐹, 𝐴)‘suc 𝑢) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))
57	56	eleq2d 2815	. . . . . . . . . . 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 37371	. . . . . . . . . 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 3133	. . . . 5 ⊢ (𝐵 ∈ 𝑊 → (∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
66	13, 65	biimtrid 242	. . . 4 ⊢ (𝐵 ∈ 𝑊 → (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
67	66	alimi 1811	. . 3 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
68		df-ral 3046	. . 3 ⊢ (∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
69	67, 68	sylibr 234	. 2 ⊢ (∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω))
70		fvex 6874	. . 3 ⊢ (rec(𝐹, 𝐴)‘ω) ∈ V
71		sseq2 3976	. . . 4 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω)))
72		nfcv 2892	. . . . . . . 8 ⊢ Ⅎ𝑦ω
73	30, 72	nffv 6871	. . . . . . 7 ⊢ Ⅎ𝑦(rec(𝐹, 𝐴)‘ω)
74	73	nfeq2 2910	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = (rec(𝐹, 𝐴)‘ω)
75		eleq2 2818	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (rec(𝐹, 𝐴)‘ω)))
76		eleq2 2818	. . . . . . 7 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))
77	75, 76	imbi12d 344	. . . . . 6 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
78	74, 77	albid 2223	. . . . 5 ⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (∀𝑦(𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))))
79		df-ral 3046	. . . . 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 3575	. 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 3045 ∃wrex 3054 Vcvv 3450 ∪ cun 3915 ⊆ wss 3917 ∅c0 4299 ∪ ciun 4958 ↦ cmpt 5191 ran crn 5642 Oncon0 6335 Lim wlim 6336 suc csuc 6337 ‘cfv 6514 ωcom 7845 reccrdg 8380

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 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pr 5390 ax-un 7714 ax-inf2 9601

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 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-ov 7393 df-om 7846 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381

This theorem is referenced by: exrecfn 37375

W3C validator