Metamath Proof Explorer

Theorem modelaxreplem3

Description: Lemma for modelaxrep . We show that the consequent of Replacement is satisfied with ran F as the value of y . (Contributed by Eric Schmidt, 29-Sep-2025)

Ref Expression
Hypotheses modelaxreplem.1 ⊢ ψ → x ⊆ M
modelaxreplem.2 ⊢ ψ → ∀ f Fun ⁡ f ∧ dom ⁡ f ∈ M ∧ ran ⁡ f ⊆ M → ran ⁡ f ∈ M
modelaxreplem.3 ⊢ ψ → ∅ ∈ M
modelaxreplem.4 ⊢ ψ → x ∈ M
modelaxreplem2.5 ⊢ Ⅎ w ψ
modelaxreplem2.6 ⊢ Ⅎ z ψ
modelaxreplem2.7 ⊢ Ⅎ _ z F
modelaxreplem2.8 ⊢ F = w z | w ∈ x ∧ z ∈ M ∧ ∀ y φ
modelaxreplem2.9 ⊢ ψ → w ∈ M → ∃ y ∈ M ∀ z ∈ M ∀ y φ → z = y
Assertion modelaxreplem3 ⊢ ψ → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ

Proof

Step Hyp Ref Expression
1 modelaxreplem.1 ⊢ ψ → x ⊆ M
2 modelaxreplem.2 ⊢ ψ → ∀ f Fun ⁡ f ∧ dom ⁡ f ∈ M ∧ ran ⁡ f ⊆ M → ran ⁡ f ∈ M
3 modelaxreplem.3 ⊢ ψ → ∅ ∈ M
4 modelaxreplem.4 ⊢ ψ → x ∈ M
5 modelaxreplem2.5 ⊢ Ⅎ w ψ
6 modelaxreplem2.6 ⊢ Ⅎ z ψ
7 modelaxreplem2.7 ⊢ Ⅎ _ z F
8 modelaxreplem2.8 ⊢ F = w z | w ∈ x ∧ z ∈ M ∧ ∀ y φ
9 modelaxreplem2.9 ⊢ ψ → w ∈ M → ∃ y ∈ M ∀ z ∈ M ∀ y φ → z = y
10 1 2 3 4 5 6 7 8 9 modelaxreplem2 ⊢ ψ → ran ⁡ F ∈ M
11 1 sseld ⊢ ψ → w ∈ x → w ∈ M
12 11 pm4.71rd ⊢ ψ → w ∈ x ↔ w ∈ M ∧ w ∈ x
13 12 anbi1d ⊢ ψ → w ∈ x ∧ z ∈ M ∧ ∀ y φ ↔ w ∈ M ∧ w ∈ x ∧ z ∈ M ∧ ∀ y φ
14 an12 ⊢ w ∈ M ∧ w ∈ x ∧ z ∈ M ∧ ∀ y φ ↔ z ∈ M ∧ w ∈ M ∧ w ∈ x ∧ ∀ y φ
15 anass ⊢ w ∈ M ∧ w ∈ x ∧ ∀ y φ ↔ w ∈ M ∧ w ∈ x ∧ ∀ y φ
16 15 anbi2i ⊢ z ∈ M ∧ w ∈ M ∧ w ∈ x ∧ ∀ y φ ↔ z ∈ M ∧ w ∈ M ∧ w ∈ x ∧ ∀ y φ
17 14 16 bitri ⊢ w ∈ M ∧ w ∈ x ∧ z ∈ M ∧ ∀ y φ ↔ z ∈ M ∧ w ∈ M ∧ w ∈ x ∧ ∀ y φ
18 13 17 bitrdi ⊢ ψ → w ∈ x ∧ z ∈ M ∧ ∀ y φ ↔ z ∈ M ∧ w ∈ M ∧ w ∈ x ∧ ∀ y φ
19 5 18 exbid ⊢ ψ → ∃ w w ∈ x ∧ z ∈ M ∧ ∀ y φ ↔ ∃ w z ∈ M ∧ w ∈ M ∧ w ∈ x ∧ ∀ y φ
20 8 rneqi ⊢ ran ⁡ F = ran ⁡ w z | w ∈ x ∧ z ∈ M ∧ ∀ y φ
21 rnopab ⊢ ran ⁡ w z | w ∈ x ∧ z ∈ M ∧ ∀ y φ = z | ∃ w w ∈ x ∧ z ∈ M ∧ ∀ y φ
22 20 21 eqtri ⊢ ran ⁡ F = z | ∃ w w ∈ x ∧ z ∈ M ∧ ∀ y φ
23 22 eqabri ⊢ z ∈ ran ⁡ F ↔ ∃ w w ∈ x ∧ z ∈ M ∧ ∀ y φ
24 df-rex ⊢ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ ∃ w w ∈ M ∧ w ∈ x ∧ ∀ y φ
25 24 anbi2i ⊢ z ∈ M ∧ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ z ∈ M ∧ ∃ w w ∈ M ∧ w ∈ x ∧ ∀ y φ
26 19.42v ⊢ ∃ w z ∈ M ∧ w ∈ M ∧ w ∈ x ∧ ∀ y φ ↔ z ∈ M ∧ ∃ w w ∈ M ∧ w ∈ x ∧ ∀ y φ
27 25 26 bitr4i ⊢ z ∈ M ∧ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ ∃ w z ∈ M ∧ w ∈ M ∧ w ∈ x ∧ ∀ y φ
28 19 23 27 3bitr4g ⊢ ψ → z ∈ ran ⁡ F ↔ z ∈ M ∧ ∃ w ∈ M w ∈ x ∧ ∀ y φ
29 28 baibd ⊢ ψ ∧ z ∈ M → z ∈ ran ⁡ F ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
30 6 29 ralrimia ⊢ ψ → ∀ z ∈ M z ∈ ran ⁡ F ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
31 7 nfrn ⊢ Ⅎ _ z ran ⁡ F
32 sbcralt ⊢ ran ⁡ F ∈ M ∧ Ⅎ _ z ran ⁡ F → [˙ ran ⁡ F / y]˙ ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ ∀ z ∈ M [˙ ran ⁡ F / y]˙ z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
33 31 32 mpan2 ⊢ ran ⁡ F ∈ M → [˙ ran ⁡ F / y]˙ ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ ∀ z ∈ M [˙ ran ⁡ F / y]˙ z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
34 31 nfel1 ⊢ Ⅎ z ran ⁡ F ∈ M
35 sbcbig ⊢ ran ⁡ F ∈ M → [˙ ran ⁡ F / y]˙ z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ [˙ ran ⁡ F / y]˙ z ∈ y ↔ [˙ ran ⁡ F / y]˙ ∃ w ∈ M w ∈ x ∧ ∀ y φ
36 sbcel2gv ⊢ ran ⁡ F ∈ M → [˙ ran ⁡ F / y]˙ z ∈ y ↔ z ∈ ran ⁡ F
37 nfcv ⊢ Ⅎ _ y M
38 nfv ⊢ Ⅎ y w ∈ x
39 nfa1 ⊢ Ⅎ y ∀ y φ
40 38 39 nfan ⊢ Ⅎ y w ∈ x ∧ ∀ y φ
41 37 40 nfrexw ⊢ Ⅎ y ∃ w ∈ M w ∈ x ∧ ∀ y φ
42 41 sbcgf ⊢ ran ⁡ F ∈ M → [˙ ran ⁡ F / y]˙ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
43 36 42 bibi12d ⊢ ran ⁡ F ∈ M → [˙ ran ⁡ F / y]˙ z ∈ y ↔ [˙ ran ⁡ F / y]˙ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ z ∈ ran ⁡ F ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
44 35 43 bitrd ⊢ ran ⁡ F ∈ M → [˙ ran ⁡ F / y]˙ z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ z ∈ ran ⁡ F ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
45 34 44 ralbid ⊢ ran ⁡ F ∈ M → ∀ z ∈ M [˙ ran ⁡ F / y]˙ z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ ∀ z ∈ M z ∈ ran ⁡ F ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
46 33 45 bitrd ⊢ ran ⁡ F ∈ M → [˙ ran ⁡ F / y]˙ ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ ∀ z ∈ M z ∈ ran ⁡ F ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
47 10 46 syl ⊢ ψ → [˙ ran ⁡ F / y]˙ ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ ↔ ∀ z ∈ M z ∈ ran ⁡ F ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
48 30 47 mpbird ⊢ ψ → [˙ ran ⁡ F / y]˙ ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ
49 10 48 rspesbcd ⊢ ψ → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y φ