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 ∧ ∀ y B ∈ W → ∃ x A ⊆ x ∧ ∀ y ∈ x B ∈ x

Proof

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