Metamath Proof Explorer

Theorem fineqvrep

Description: If the Axiom of Infinity is negated, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024)

Ref Expression
Assertion fineqvrep ⊢ Fin = V → ∀ w ∃ y ∀ z ∀ y φ → z = y → ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ

Proof

Step Hyp Ref Expression
1 funopab ⊢ Fun ⁡ w z | ∀ y φ ↔ ∀ w ∃* z ∀ y φ
2 nfa1 ⊢ Ⅎ y ∀ y φ
3 2 mof ⊢ ∃* z ∀ y φ ↔ ∃ y ∀ z ∀ y φ → z = y
4 3 albii ⊢ ∀ w ∃* z ∀ y φ ↔ ∀ w ∃ y ∀ z ∀ y φ → z = y
5 1 4 bitr2i ⊢ ∀ w ∃ y ∀ z ∀ y φ → z = y ↔ Fun ⁡ w z | ∀ y φ
6 vex ⊢ x ∈ V
7 eleq2w2 ⊢ Fin = V → x ∈ Fin ↔ x ∈ V
8 6 7 mpbiri ⊢ Fin = V → x ∈ Fin
9 imafi ⊢ Fun ⁡ w z | ∀ y φ ∧ x ∈ Fin → w z | ∀ y φ x ∈ Fin
10 8 9 sylan2 ⊢ Fun ⁡ w z | ∀ y φ ∧ Fin = V → w z | ∀ y φ x ∈ Fin
11 10 elexd ⊢ Fun ⁡ w z | ∀ y φ ∧ Fin = V → w z | ∀ y φ x ∈ V
12 nfv ⊢ Ⅎ y w ∈ x
13 2 nfopab ⊢ Ⅎ _ y w z | ∀ y φ
14 13 nfel2 ⊢ Ⅎ y w z ∈ w z | ∀ y φ
15 12 14 nfan ⊢ Ⅎ y w ∈ x ∧ w z ∈ w z | ∀ y φ
16 15 nfex ⊢ Ⅎ y ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
17 16 nfab ⊢ Ⅎ _ y z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
18 17 issetf ⊢ z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ∈ V ↔ ∃ y y = z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
19 abeq2 ⊢ y = z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ↔ ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
20 19 exbii ⊢ ∃ y y = z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ↔ ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
21 opabidw ⊢ w z ∈ w z | ∀ y φ ↔ ∀ y φ
22 21 anbi2i ⊢ w ∈ x ∧ w z ∈ w z | ∀ y φ ↔ w ∈ x ∧ ∀ y φ
23 22 exbii ⊢ ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ↔ ∃ w w ∈ x ∧ ∀ y φ
24 23 bibi2i ⊢ z ∈ y ↔ ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ↔ z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
25 24 albii ⊢ ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ↔ ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
26 25 exbii ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ↔ ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
27 18 20 26 3bitrri ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ ↔ z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ∈ V
28 dfima3 ⊢ w z | ∀ y φ x = v | ∃ u u ∈ x ∧ u v ∈ w z | ∀ y φ
29 nfv ⊢ Ⅎ z u ∈ x
30 nfopab2 ⊢ Ⅎ _ z w z | ∀ y φ
31 30 nfel2 ⊢ Ⅎ z u v ∈ w z | ∀ y φ
32 29 31 nfan ⊢ Ⅎ z u ∈ x ∧ u v ∈ w z | ∀ y φ
33 32 nfex ⊢ Ⅎ z ∃ u u ∈ x ∧ u v ∈ w z | ∀ y φ
34 nfv ⊢ Ⅎ v ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
35 nfv ⊢ Ⅎ w u ∈ x
36 nfopab1 ⊢ Ⅎ _ w w z | ∀ y φ
37 36 nfel2 ⊢ Ⅎ w u v ∈ w z | ∀ y φ
38 35 37 nfan ⊢ Ⅎ w u ∈ x ∧ u v ∈ w z | ∀ y φ
39 nfv ⊢ Ⅎ u w ∈ x ∧ w v ∈ w z | ∀ y φ
40 elequ1 ⊢ u = w → u ∈ x ↔ w ∈ x
41 opeq1 ⊢ u = w → u v = w v
42 41 eleq1d ⊢ u = w → u v ∈ w z | ∀ y φ ↔ w v ∈ w z | ∀ y φ
43 40 42 anbi12d ⊢ u = w → u ∈ x ∧ u v ∈ w z | ∀ y φ ↔ w ∈ x ∧ w v ∈ w z | ∀ y φ
44 38 39 43 cbvexv1 ⊢ ∃ u u ∈ x ∧ u v ∈ w z | ∀ y φ ↔ ∃ w w ∈ x ∧ w v ∈ w z | ∀ y φ
45 opeq2 ⊢ v = z → w v = w z
46 45 eleq1d ⊢ v = z → w v ∈ w z | ∀ y φ ↔ w z ∈ w z | ∀ y φ
47 46 anbi2d ⊢ v = z → w ∈ x ∧ w v ∈ w z | ∀ y φ ↔ w ∈ x ∧ w z ∈ w z | ∀ y φ
48 47 exbidv ⊢ v = z → ∃ w w ∈ x ∧ w v ∈ w z | ∀ y φ ↔ ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
49 44 48 syl5bb ⊢ v = z → ∃ u u ∈ x ∧ u v ∈ w z | ∀ y φ ↔ ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
50 33 34 49 cbvabw ⊢ v | ∃ u u ∈ x ∧ u v ∈ w z | ∀ y φ = z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
51 28 50 eqtri ⊢ w z | ∀ y φ x = z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ
52 51 eleq1i ⊢ w z | ∀ y φ x ∈ V ↔ z | ∃ w w ∈ x ∧ w z ∈ w z | ∀ y φ ∈ V
53 27 52 bitr4i ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ ↔ w z | ∀ y φ x ∈ V
54 11 53 sylibr ⊢ Fun ⁡ w z | ∀ y φ ∧ Fin = V → ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
55 5 54 sylanb ⊢ ∀ w ∃ y ∀ z ∀ y φ → z = y ∧ Fin = V → ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
56 55 expcom ⊢ Fin = V → ∀ w ∃ y ∀ z ∀ y φ → z = y → ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ