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

Metamath Proof Explorer

Theorem opabiotafun

Description: Define a function whose value is "the unique y such that ph ( x , y ) ". (Contributed by NM, 19-May-2015)

Ref Expression
Hypothesis opabiota.1 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
Assertion opabiotafun Fun 𝐹

Proof

Step Hyp Ref Expression
1 opabiota.1 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
2 funopab ⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } } ↔ ∀ 𝑥 ∃* 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 } )
3 mo2icl ⊢ ( ∀ 𝑧 ( { 𝑦 ∣ 𝜑 } = { 𝑧 } → 𝑧 = ∪ { 𝑦 ∣ 𝜑 } ) → ∃* 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑧 } )
4 unieq ⊢ ( { 𝑦 ∣ 𝜑 } = { 𝑧 } → ∪ { 𝑦 ∣ 𝜑 } = ∪ { 𝑧 } )
5 unisnv ⊢ ∪ { 𝑧 } = 𝑧
6 4 5 eqtr2di ⊢ ( { 𝑦 ∣ 𝜑 } = { 𝑧 } → 𝑧 = ∪ { 𝑦 ∣ 𝜑 } )
7 3 6 mpg ⊢ ∃* 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑧 }
8 nfv ⊢ Ⅎ 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑦 }
9 nfab1 ⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 }
10 9 nfeq1 ⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑧 }
11 sneq ⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
12 11 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( { 𝑦 ∣ 𝜑 } = { 𝑦 } ↔ { 𝑦 ∣ 𝜑 } = { 𝑧 } ) )
13 8 10 12 cbvmow ⊢ ( ∃* 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 } ↔ ∃* 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑧 } )
14 7 13 mpbir ⊢ ∃* 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 }
15 2 14 mpgbir ⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
16 1 funeqi ⊢ ( Fun 𝐹 ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } } )
17 15 16 mpbir ⊢ Fun 𝐹