Metamath Proof Explorer

Theorem vsmrep

Description: The universe is a standard model of the strong Axiom Scheme of Replacement. (Contributed by BTernaryTau, 2-Oct-2026)

Ref Expression
Assertion vsmrep V ⊨ Ax-Rep*

Proof

Step Hyp Ref Expression
1 df-smrep ⊢ ( V ⊨ Ax-Rep* ↔ ∀ 𝑓 ∀ 𝑥 ∈ V ( ∀ 𝑤 ∈ V ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
2 ax-rep ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
3 ralv ⊢ ( ∀ 𝑤 ∈ V ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
4 rexv ⊢ ( ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
5 ralv ⊢ ( ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
6 5 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
7 4 6 bitri ⊢ ( ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
8 7 albii ⊢ ( ∀ 𝑤 ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
9 3 8 bitri ⊢ ( ∀ 𝑤 ∈ V ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
10 rexv ⊢ ( ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
11 ralv ⊢ ( ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
12 rexv ⊢ ( ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) )
13 12 bibi2i ⊢ ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
14 13 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
15 11 14 bitri ⊢ ( ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
16 15 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
17 10 16 bitri ⊢ ( ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
18 2 9 17 3imtr4i ⊢ ( ∀ 𝑤 ∈ V ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
19 18 rgenw ⊢ ∀ 𝑥 ∈ V ( ∀ 𝑤 ∈ V ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ V ∀ 𝑧 ∈ V ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
20 1 19 mpgbir ⊢ V ⊨ Ax-Rep*