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 imbitrrid ⊢ ( 𝑢 ∈ 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 biimtrid ⊢ ( 𝐵 ∈ 𝑊 → ( 𝑦 ∈ ( 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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 𝐵 ∈ 𝑊 ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝐵 ∈ 𝑥 ) )