Metamath Proof Explorer

Theorem fineqvrep

Description: If all sets are finite, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024)

Ref Expression
Assertion fineqvrep ( Fin = V → ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 funopab ⊢ ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ↔ ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 )
2 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑
3 2 mof ⊢ ( ∃* 𝑧 ∀ 𝑦 𝜑 ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) )
4 3 albii ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) )
5 1 4 bitr2i ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } )
6 vex ⊢ 𝑥 ∈ V
7 eleq2w2 ⊢ ( Fin = V → ( 𝑥 ∈ Fin ↔ 𝑥 ∈ V ) )
8 6 7 mpbiri ⊢ ( Fin = V → 𝑥 ∈ Fin )
9 imafi ⊢ ( ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ∧ 𝑥 ∈ Fin ) → ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } “ 𝑥 ) ∈ Fin )
10 8 9 sylan2 ⊢ ( ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ∧ Fin = V ) → ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } “ 𝑥 ) ∈ Fin )
11 10 elexd ⊢ ( ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ∧ Fin = V ) → ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } “ 𝑥 ) ∈ V )
12 nfv ⊢ Ⅎ 𝑦 𝑤 ∈ 𝑥
13 2 nfopab ⊢ Ⅎ 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 }
14 13 nfel2 ⊢ Ⅎ 𝑦 ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 }
15 12 14 nfan ⊢ Ⅎ 𝑦 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } )
16 15 nfex ⊢ Ⅎ 𝑦 ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } )
17 16 nfab ⊢ Ⅎ 𝑦 { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) }
18 17 issetf ⊢ ( { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) } ∈ V ↔ ∃ 𝑦 𝑦 = { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) } )
19 eqabb ⊢ ( 𝑦 = { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) } ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) )
20 19 exbii ⊢ ( ∃ 𝑦 𝑦 = { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) } ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) )
21 opabidw ⊢ ( ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ↔ ∀ 𝑦 𝜑 )
22 21 anbi2i ⊢ ( ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ↔ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) )
23 22 exbii ⊢ ( ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) )
24 23 bibi2i ⊢ ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) ↔ ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
25 24 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
26 25 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
27 18 20 26 3bitrri ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) } ∈ V )
28 dfima3 ⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } “ 𝑥 ) = { 𝑣 ∣ ∃ 𝑢 ( 𝑢 ∈ 𝑥 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) }
29 nfv ⊢ Ⅎ 𝑧 𝑢 ∈ 𝑥
30 nfopab2 ⊢ Ⅎ 𝑧 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 }
31 30 nfel2 ⊢ Ⅎ 𝑧 ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 }
32 29 31 nfan ⊢ Ⅎ 𝑧 ( 𝑢 ∈ 𝑥 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } )
33 32 nfex ⊢ Ⅎ 𝑧 ∃ 𝑢 ( 𝑢 ∈ 𝑥 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } )
34 nfv ⊢ Ⅎ 𝑣 ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } )
35 nfv ⊢ Ⅎ 𝑤 𝑢 ∈ 𝑥
36 nfopab1 ⊢ Ⅎ 𝑤 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 }
37 36 nfel2 ⊢ Ⅎ 𝑤 ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 }
38 35 37 nfan ⊢ Ⅎ 𝑤 ( 𝑢 ∈ 𝑥 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } )
39 nfv ⊢ Ⅎ 𝑢 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } )
40 elequ1 ⊢ ( 𝑢 = 𝑤 → ( 𝑢 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥 ) )
41 opeq1 ⊢ ( 𝑢 = 𝑤 → ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ )
42 41 eleq1d ⊢ ( 𝑢 = 𝑤 → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ↔ ⟨ 𝑤 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) )
43 40 42 anbi12d ⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 ∈ 𝑥 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ↔ ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) )
44 38 39 43 cbvexv1 ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑥 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) )
45 opeq2 ⊢ ( 𝑣 = 𝑧 → ⟨ 𝑤 , 𝑣 ⟩ = ⟨ 𝑤 , 𝑧 ⟩ )
46 45 eleq1d ⊢ ( 𝑣 = 𝑧 → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ↔ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) )
47 46 anbi2d ⊢ ( 𝑣 = 𝑧 → ( ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ↔ ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) )
48 47 exbidv ⊢ ( 𝑣 = 𝑧 → ( ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) )
49 44 48 bitrid ⊢ ( 𝑣 = 𝑧 → ( ∃ 𝑢 ( 𝑢 ∈ 𝑥 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) ) )
50 33 34 49 cbvabw ⊢ { 𝑣 ∣ ∃ 𝑢 ( 𝑢 ∈ 𝑥 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) } = { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) }
51 28 50 eqtri ⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } “ 𝑥 ) = { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) }
52 51 eleq1i ⊢ ( ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } “ 𝑥 ) ∈ V ↔ { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ) } ∈ V )
53 27 52 bitr4i ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } “ 𝑥 ) ∈ V )
54 11 53 sylibr ⊢ ( ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∀ 𝑦 𝜑 } ∧ Fin = V ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
55 5 54 sylanb ⊢ ( ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ∧ Fin = V ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
56 55 expcom ⊢ ( Fin = V → ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )