Metamath Proof Explorer


Theorem exrecfnlem

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

Ref Expression
Hypothesis exrecfnlem.1 𝐹 = ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) ) )
Assertion exrecfnlem ( ( 𝐴𝑉 ∧ ∀ 𝑦 𝐵𝑊 ) → ∃ 𝑥 ( 𝐴𝑥 ∧ ∀ 𝑦𝑥 𝐵𝑥 ) )

Proof

Step Hyp Ref Expression
1 exrecfnlem.1 𝐹 = ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) ) )
2 rdg0g ( 𝐴𝑉 → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴 )
3 peano1 ∅ ∈ ω
4 omelon ω ∈ On
5 limom Lim ω
6 rdglimss ( ( ( ω ∈ On ∧ Lim ω ) ∧ ∅ ∈ ω ) → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) )
7 4 5 6 mpanl12 ( ∅ ∈ ω → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) )
8 3 7 ax-mp ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ ω )
9 2 8 eqsstrrdi ( 𝐴𝑉𝐴 ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) )
10 rdglim2a ( ( ω ∈ On ∧ Lim ω ) → ( rec ( 𝐹 , 𝐴 ) ‘ ω ) = 𝑢 ∈ ω ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) )
11 4 5 10 mp2an ( rec ( 𝐹 , 𝐴 ) ‘ ω ) = 𝑢 ∈ ω ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 )
12 11 eleq2i ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ↔ 𝑦 𝑢 ∈ ω ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) )
13 eliun ( 𝑦 𝑢 ∈ ω ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↔ ∃ 𝑢 ∈ ω 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) )
14 12 13 bitri ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ↔ ∃ 𝑢 ∈ ω 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) )
15 peano2 ( 𝑢 ∈ ω → suc 𝑢 ∈ ω )
16 nnon ( 𝑢 ∈ ω → 𝑢 ∈ On )
17 eqid ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) = ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 )
18 17 elrnmpt1 ( ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∧ 𝐵𝑊 ) → 𝐵 ∈ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) )
19 elun2 ( 𝐵 ∈ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) → 𝐵 ∈ ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ) )
20 18 19 syl ( ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∧ 𝐵𝑊 ) → 𝐵 ∈ ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ) )
21 fvex ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∈ V
22 nfcv 𝑦 V
23 nfcv 𝑦 𝑧
24 nfmpt1 𝑦 ( 𝑦𝑧𝐵 )
25 24 nfrn 𝑦 ran ( 𝑦𝑧𝐵 )
26 23 25 nfun 𝑦 ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) )
27 22 26 nfmpt 𝑦 ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) ) )
28 1 27 nfcxfr 𝑦 𝐹
29 nfcv 𝑦 𝐴
30 28 29 nfrdg 𝑦 rec ( 𝐹 , 𝐴 )
31 nfcv 𝑦 𝑢
32 30 31 nffv 𝑦 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 )
33 32 mptexgf ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∈ V → ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ∈ V )
34 21 33 ax-mp ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ∈ V
35 34 rnex ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ∈ V
36 21 35 unex ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ) ∈ V
37 nfcv 𝑧 𝐴
38 nfcv 𝑧 𝑢
39 nfmpt1 𝑧 ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) ) )
40 1 39 nfcxfr 𝑧 𝐹
41 40 37 nfrdg 𝑧 rec ( 𝐹 , 𝐴 )
42 41 38 nffv 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 )
43 nfcv 𝑧 𝐵
44 42 43 nfmpt 𝑧 ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 )
45 44 nfrn 𝑧 ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 )
46 42 45 nfun 𝑧 ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) )
47 rdgeq1 ( 𝐹 = ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) ) ) → rec ( 𝐹 , 𝐴 ) = rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) ) ) , 𝐴 ) )
48 1 47 ax-mp rec ( 𝐹 , 𝐴 ) = rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) ) ) , 𝐴 )
49 id ( 𝑧 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) → 𝑧 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) )
50 32 nfeq2 𝑦 𝑧 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 )
51 eqidd ( 𝑧 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) → 𝐵 = 𝐵 )
52 50 49 51 mpteq12df ( 𝑧 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) → ( 𝑦𝑧𝐵 ) = ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) )
53 52 rneqd ( 𝑧 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) → ran ( 𝑦𝑧𝐵 ) = ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) )
54 49 53 uneq12d ( 𝑧 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) → ( 𝑧 ∪ ran ( 𝑦𝑧𝐵 ) ) = ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ) )
55 37 38 46 48 54 rdgsucmptf ( ( 𝑢 ∈ On ∧ ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ) ∈ V ) → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑢 ) = ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ) )
56 36 55 mpan2 ( 𝑢 ∈ On → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑢 ) = ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ) )
57 56 eleq2d ( 𝑢 ∈ On → ( 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑢 ) ↔ 𝐵 ∈ ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∪ ran ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ↦ 𝐵 ) ) ) )
58 20 57 syl5ibr ( 𝑢 ∈ On → ( ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∧ 𝐵𝑊 ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑢 ) ) )
59 16 58 syl ( 𝑢 ∈ ω → ( ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∧ 𝐵𝑊 ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑢 ) ) )
60 rdgellim ( ( ( ω ∈ On ∧ Lim ω ) ∧ suc 𝑢 ∈ ω ) → ( 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑢 ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
61 4 5 60 mpanl12 ( suc 𝑢 ∈ ω → ( 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑢 ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
62 15 59 61 sylsyld ( 𝑢 ∈ ω → ( ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) ∧ 𝐵𝑊 ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
63 62 expd ( 𝑢 ∈ ω → ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) → ( 𝐵𝑊𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) ) )
64 63 com3r ( 𝐵𝑊 → ( 𝑢 ∈ ω → ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) ) )
65 64 rexlimdv ( 𝐵𝑊 → ( ∃ 𝑢 ∈ ω 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑢 ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
66 14 65 syl5bi ( 𝐵𝑊 → ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
67 66 alimi ( ∀ 𝑦 𝐵𝑊 → ∀ 𝑦 ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
68 df-ral ( ∀ 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ↔ ∀ 𝑦 ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
69 67 68 sylibr ( ∀ 𝑦 𝐵𝑊 → ∀ 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) )
70 fvex ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ∈ V
71 sseq2 ( 𝑥 = ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → ( 𝐴𝑥𝐴 ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
72 nfcv 𝑦 ω
73 30 72 nffv 𝑦 ( rec ( 𝐹 , 𝐴 ) ‘ ω )
74 73 nfeq2 𝑦 𝑥 = ( rec ( 𝐹 , 𝐴 ) ‘ ω )
75 eleq2 ( 𝑥 = ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → ( 𝑦𝑥𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
76 eleq2 ( 𝑥 = ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → ( 𝐵𝑥𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
77 75 76 imbi12d ( 𝑥 = ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → ( ( 𝑦𝑥𝐵𝑥 ) ↔ ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) ) )
78 74 77 albid ( 𝑥 = ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → ( ∀ 𝑦 ( 𝑦𝑥𝐵𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) ) )
79 df-ral ( ∀ 𝑦𝑥 𝐵𝑥 ↔ ∀ 𝑦 ( 𝑦𝑥𝐵𝑥 ) )
80 78 79 68 3bitr4g ( 𝑥 = ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → ( ∀ 𝑦𝑥 𝐵𝑥 ↔ ∀ 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) )
81 71 80 anbi12d ( 𝑥 = ( rec ( 𝐹 , 𝐴 ) ‘ ω ) → ( ( 𝐴𝑥 ∧ ∀ 𝑦𝑥 𝐵𝑥 ) ↔ ( 𝐴 ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ∧ ∀ 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) ) )
82 70 81 spcev ( ( 𝐴 ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ∧ ∀ 𝑦 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ ω ) ) → ∃ 𝑥 ( 𝐴𝑥 ∧ ∀ 𝑦𝑥 𝐵𝑥 ) )
83 9 69 82 syl2an ( ( 𝐴𝑉 ∧ ∀ 𝑦 𝐵𝑊 ) → ∃ 𝑥 ( 𝐴𝑥 ∧ ∀ 𝑦𝑥 𝐵𝑥 ) )