This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zfrep6

Description: A version of the Axiom of Replacement. Normally ph would have free variables x and y . Axiom 6 of Kunen p. 12. The Separation Scheme ax-sep cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep . (Contributed by NM, 10-Oct-2003)

Ref Expression
Assertion zfrep6 ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )

Proof

Step Hyp Ref Expression
1 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ ∃ 𝑦 𝜑 ) )
2 1 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝑧 ∧ ∃ 𝑦 𝜑 ) }
3 dmopab ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
4 df-rab ⊢ { 𝑥 ∈ 𝑧 ∣ ∃ 𝑦 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑧 ∧ ∃ 𝑦 𝜑 ) }
5 2 3 4 3eqtr4i ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } = { 𝑥 ∈ 𝑧 ∣ ∃ 𝑦 𝜑 }
6 euex ⊢ ( ∃! 𝑦 𝜑 → ∃ 𝑦 𝜑 )
7 6 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 )
8 rabid2 ⊢ ( 𝑧 = { 𝑥 ∈ 𝑧 ∣ ∃ 𝑦 𝜑 } ↔ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 )
9 7 8 sylibr ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → 𝑧 = { 𝑥 ∈ 𝑧 ∣ ∃ 𝑦 𝜑 } )
10 5 9 eqtr4id ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } = 𝑧 )
11 vex ⊢ 𝑧 ∈ V
12 10 11 eqeltrdi ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∈ V )
13 eumo ⊢ ( ∃! 𝑦 𝜑 → ∃* 𝑦 𝜑 )
14 13 imim2i ⊢ ( ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ( 𝑥 ∈ 𝑧 → ∃* 𝑦 𝜑 ) )
15 moanimv ⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 → ∃* 𝑦 𝜑 ) )
16 14 15 sylibr ⊢ ( ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
17 16 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
18 df-ral ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) )
19 funopab ⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
20 17 18 19 3imtr4i ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } )
21 funrnex ⊢ ( dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∈ V → ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∈ V ) )
22 12 20 21 sylc ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∈ V )
23 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑
24 10 eleq2d ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ( 𝑥 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ↔ 𝑥 ∈ 𝑧 ) )
25 opabidw ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
26 vex ⊢ 𝑥 ∈ V
27 vex ⊢ 𝑦 ∈ V
28 26 27 opelrn ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } )
29 25 28 sylbir ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } )
30 29 ex ⊢ ( 𝑥 ∈ 𝑧 → ( 𝜑 → 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ) )
31 30 impac ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → ( 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∧ 𝜑 ) )
32 31 eximi ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → ∃ 𝑦 ( 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∧ 𝜑 ) )
33 3 eqabri ⊢ ( 𝑥 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
34 df-rex ⊢ ( ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∧ 𝜑 ) )
35 32 33 34 3imtr4i ⊢ ( 𝑥 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 )
36 24 35 biimtrrdi ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ( 𝑥 ∈ 𝑧 → ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 ) )
37 23 36 ralrimi ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 )
38 nfopab1 ⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
39 38 nfrn ⊢ Ⅎ 𝑥 ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
40 39 nfeq2 ⊢ Ⅎ 𝑥 𝑤 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
41 nfcv ⊢ Ⅎ 𝑦 𝑤
42 nfopab2 ⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
43 42 nfrn ⊢ Ⅎ 𝑦 ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
44 41 43 rexeqf ⊢ ( 𝑤 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → ( ∃ 𝑦 ∈ 𝑤 𝜑 ↔ ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 ) )
45 40 44 ralbid ⊢ ( 𝑤 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 ↔ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 ) )
46 22 37 45 spcedv ⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )