Metamath Proof Explorer

Theorem bnj1366

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1366.1 ⊢ ( 𝜓 ↔ ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ∧ 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ) )
Assertion bnj1366 ( 𝜓 → 𝐵 ∈ V )

Proof

Step Hyp Ref Expression
1 bnj1366.1 ⊢ ( 𝜓 ↔ ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ∧ 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ) )
2 1 simp3bi ⊢ ( 𝜓 → 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } )
3 1 simp2bi ⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 )
4 nfcv ⊢ Ⅎ 𝑦 𝐴
5 nfeu1 ⊢ Ⅎ 𝑦 ∃! 𝑦 𝜑
6 4 5 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑
7 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑
8 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑦 𝜑 )
9 iota1 ⊢ ( ∃! 𝑦 𝜑 → ( 𝜑 ↔ ( ℩ 𝑦 𝜑 ) = 𝑦 ) )
10 eqcom ⊢ ( ( ℩ 𝑦 𝜑 ) = 𝑦 ↔ 𝑦 = ( ℩ 𝑦 𝜑 ) )
11 9 10 bitrdi ⊢ ( ∃! 𝑦 𝜑 → ( 𝜑 ↔ 𝑦 = ( ℩ 𝑦 𝜑 ) ) )
12 8 11 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ↔ 𝑦 = ( ℩ 𝑦 𝜑 ) ) )
13 7 12 rexbida ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( ℩ 𝑦 𝜑 ) ) )
14 abid ⊢ ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
15 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) )
16 iotaex ⊢ ( ℩ 𝑦 𝜑 ) ∈ V
17 15 16 elrnmpti ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( ℩ 𝑦 𝜑 ) )
18 13 14 17 3bitr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 → ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ) )
19 6 18 alrimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 → ∀ 𝑦 ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ) )
20 3 19 syl ⊢ ( 𝜓 → ∀ 𝑦 ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ) )
21 nfab1 ⊢ Ⅎ 𝑦 { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }
22 nfiota1 ⊢ Ⅎ 𝑦 ( ℩ 𝑦 𝜑 )
23 4 22 nfmpt ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) )
24 23 nfrn ⊢ Ⅎ 𝑦 ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) )
25 21 24 cleqf ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } = ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ) )
26 20 25 sylibr ⊢ ( 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } = ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) )
27 2 26 eqtrd ⊢ ( 𝜓 → 𝐵 = ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) )
28 1 simp1bi ⊢ ( 𝜓 → 𝐴 ∈ V )
29 mptexg ⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ∈ V )
30 rnexg ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ∈ V → ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ∈ V )
31 28 29 30 3syl ⊢ ( 𝜓 → ran ( 𝑥 ∈ 𝐴 ↦ ( ℩ 𝑦 𝜑 ) ) ∈ V )
32 27 31 eqeltrd ⊢ ( 𝜓 → 𝐵 ∈ V )