Metamath Proof Explorer

Theorem exrecfnlem

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

Ref Expression
Hypothesis exrecfnlem.1 ⊢F=z∈V⟼z∪ran⁡y∈z⟼B
Assertion exrecfnlem ⊢A∈V∧∀yB∈W→∃xA⊆x∧∀y∈xB∈x

Proof

Step Hyp Ref Expression
1 exrecfnlem.1 ⊢F=z∈V⟼z∪ran⁡y∈z⟼B
2 rdg0g ⊢A∈V→rec⁡FA⁡∅=A
3 peano1 ⊢∅∈ω
4 omelon ⊢ω∈On
5 limom ⊢Lim⁡ω
6 rdglimss ⊢ω∈On∧Lim⁡ω∧∅∈ω→rec⁡FA⁡∅⊆rec⁡FA⁡ω
7 4 5 6 mpanl12 ⊢∅∈ω→rec⁡FA⁡∅⊆rec⁡FA⁡ω
8 3 7 ax-mp ⊢rec⁡FA⁡∅⊆rec⁡FA⁡ω
9 2 8 eqsstrrdi ⊢A∈V→A⊆rec⁡FA⁡ω
10 rdglim2a ⊢ω∈On∧Lim⁡ω→rec⁡FA⁡ω=⋃u∈ωrec⁡FA⁡u
11 4 5 10 mp2an ⊢rec⁡FA⁡ω=⋃u∈ωrec⁡FA⁡u
12 11 eleq2i ⊢y∈rec⁡FA⁡ω↔y∈⋃u∈ωrec⁡FA⁡u
13 eliun ⊢y∈⋃u∈ωrec⁡FA⁡u↔∃u∈ωy∈rec⁡FA⁡u
14 12 13 bitri ⊢y∈rec⁡FA⁡ω↔∃u∈ωy∈rec⁡FA⁡u
15 peano2 ⊢u∈ω→suc⁡u∈ω
16 nnon ⊢u∈ω→u∈On
17 eqid ⊢y∈rec⁡FA⁡u⟼B=y∈rec⁡FA⁡u⟼B
18 17 elrnmpt1 ⊢y∈rec⁡FA⁡u∧B∈W→B∈ran⁡y∈rec⁡FA⁡u⟼B
19 elun2 ⊢B∈ran⁡y∈rec⁡FA⁡u⟼B→B∈rec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B
20 18 19 syl ⊢y∈rec⁡FA⁡u∧B∈W→B∈rec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B
21 fvex ⊢rec⁡FA⁡u∈V
22 nfcv ⊢Ⅎ_yV
23 nfcv ⊢Ⅎ_yz
24 nfmpt1 ⊢Ⅎ_yy∈z⟼B
25 24 nfrn ⊢Ⅎ_yran⁡y∈z⟼B
26 23 25 nfun ⊢Ⅎ_yz∪ran⁡y∈z⟼B
27 22 26 nfmpt ⊢Ⅎ_yz∈V⟼z∪ran⁡y∈z⟼B
28 1 27 nfcxfr ⊢Ⅎ_yF
29 nfcv ⊢Ⅎ_yA
30 28 29 nfrdg ⊢Ⅎ_yrec⁡FA
31 nfcv ⊢Ⅎ_yu
32 30 31 nffv ⊢Ⅎ_yrec⁡FA⁡u
33 32 mptexgf ⊢rec⁡FA⁡u∈V→y∈rec⁡FA⁡u⟼B∈V
34 21 33 ax-mp ⊢y∈rec⁡FA⁡u⟼B∈V
35 34 rnex ⊢ran⁡y∈rec⁡FA⁡u⟼B∈V
36 21 35 unex ⊢rec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B∈V
37 nfcv ⊢Ⅎ_zA
38 nfcv ⊢Ⅎ_zu
39 nfmpt1 ⊢Ⅎ_zz∈V⟼z∪ran⁡y∈z⟼B
40 1 39 nfcxfr ⊢Ⅎ_zF
41 40 37 nfrdg ⊢Ⅎ_zrec⁡FA
42 41 38 nffv ⊢Ⅎ_zrec⁡FA⁡u
43 nfcv ⊢Ⅎ_zB
44 42 43 nfmpt ⊢Ⅎ_zy∈rec⁡FA⁡u⟼B
45 44 nfrn ⊢Ⅎ_zran⁡y∈rec⁡FA⁡u⟼B
46 42 45 nfun ⊢Ⅎ_zrec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B
47 rdgeq1 ⊢F=z∈V⟼z∪ran⁡y∈z⟼B→rec⁡FA=rec⁡z∈V⟼z∪ran⁡y∈z⟼BA
48 1 47 ax-mp ⊢rec⁡FA=rec⁡z∈V⟼z∪ran⁡y∈z⟼BA
49 id ⊢z=rec⁡FA⁡u→z=rec⁡FA⁡u
50 32 nfeq2 ⊢Ⅎyz=rec⁡FA⁡u
51 eqidd ⊢z=rec⁡FA⁡u→B=B
52 50 49 51 mpteq12df ⊢z=rec⁡FA⁡u→y∈z⟼B=y∈rec⁡FA⁡u⟼B
53 52 rneqd ⊢z=rec⁡FA⁡u→ran⁡y∈z⟼B=ran⁡y∈rec⁡FA⁡u⟼B
54 49 53 uneq12d ⊢z=rec⁡FA⁡u→z∪ran⁡y∈z⟼B=rec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B
55 37 38 46 48 54 rdgsucmptf ⊢u∈On∧rec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B∈V→rec⁡FA⁡suc⁡u=rec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B
56 36 55 mpan2 ⊢u∈On→rec⁡FA⁡suc⁡u=rec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B
57 56 eleq2d ⊢u∈On→B∈rec⁡FA⁡suc⁡u↔B∈rec⁡FA⁡u∪ran⁡y∈rec⁡FA⁡u⟼B
58 20 57 imbitrrid ⊢u∈On→y∈rec⁡FA⁡u∧B∈W→B∈rec⁡FA⁡suc⁡u
59 16 58 syl ⊢u∈ω→y∈rec⁡FA⁡u∧B∈W→B∈rec⁡FA⁡suc⁡u
60 rdgellim ⊢ω∈On∧Lim⁡ω∧suc⁡u∈ω→B∈rec⁡FA⁡suc⁡u→B∈rec⁡FA⁡ω
61 4 5 60 mpanl12 ⊢suc⁡u∈ω→B∈rec⁡FA⁡suc⁡u→B∈rec⁡FA⁡ω
62 15 59 61 sylsyld ⊢u∈ω→y∈rec⁡FA⁡u∧B∈W→B∈rec⁡FA⁡ω
63 62 expd ⊢u∈ω→y∈rec⁡FA⁡u→B∈W→B∈rec⁡FA⁡ω
64 63 com3r ⊢B∈W→u∈ω→y∈rec⁡FA⁡u→B∈rec⁡FA⁡ω
65 64 rexlimdv ⊢B∈W→∃u∈ωy∈rec⁡FA⁡u→B∈rec⁡FA⁡ω
66 14 65 biimtrid ⊢B∈W→y∈rec⁡FA⁡ω→B∈rec⁡FA⁡ω
67 66 alimi ⊢∀yB∈W→∀yy∈rec⁡FA⁡ω→B∈rec⁡FA⁡ω
68 df-ral ⊢∀y∈rec⁡FA⁡ωB∈rec⁡FA⁡ω↔∀yy∈rec⁡FA⁡ω→B∈rec⁡FA⁡ω
69 67 68 sylibr ⊢∀yB∈W→∀y∈rec⁡FA⁡ωB∈rec⁡FA⁡ω
70 fvex ⊢rec⁡FA⁡ω∈V
71 sseq2 ⊢x=rec⁡FA⁡ω→A⊆x↔A⊆rec⁡FA⁡ω
72 nfcv ⊢Ⅎ_yω
73 30 72 nffv ⊢Ⅎ_yrec⁡FA⁡ω
74 73 nfeq2 ⊢Ⅎyx=rec⁡FA⁡ω
75 eleq2 ⊢x=rec⁡FA⁡ω→y∈x↔y∈rec⁡FA⁡ω
76 eleq2 ⊢x=rec⁡FA⁡ω→B∈x↔B∈rec⁡FA⁡ω
77 75 76 imbi12d ⊢x=rec⁡FA⁡ω→y∈x→B∈x↔y∈rec⁡FA⁡ω→B∈rec⁡FA⁡ω
78 74 77 albid ⊢x=rec⁡FA⁡ω→∀yy∈x→B∈x↔∀yy∈rec⁡FA⁡ω→B∈rec⁡FA⁡ω
79 df-ral ⊢∀y∈xB∈x↔∀yy∈x→B∈x
80 78 79 68 3bitr4g ⊢x=rec⁡FA⁡ω→∀y∈xB∈x↔∀y∈rec⁡FA⁡ωB∈rec⁡FA⁡ω
81 71 80 anbi12d ⊢x=rec⁡FA⁡ω→A⊆x∧∀y∈xB∈x↔A⊆rec⁡FA⁡ω∧∀y∈rec⁡FA⁡ωB∈rec⁡FA⁡ω
82 70 81 spcev ⊢A⊆rec⁡FA⁡ω∧∀y∈rec⁡FA⁡ωB∈rec⁡FA⁡ω→∃xA⊆x∧∀y∈xB∈x
83 9 69 82 syl2an ⊢A∈V∧∀yB∈W→∃xA⊆x∧∀y∈xB∈x