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

Metamath Proof Explorer

Theorem funcnv3

Description: A condition showing a class is single-rooted. (See funcnv ). (Contributed by NM, 26-May-2006)

Ref Expression
Assertion funcnv3 ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∈ ran 𝐴 ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 )

Proof

Step Hyp Ref Expression
1 dfrn2 ⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }
2 1 eqabri ⊢ ( 𝑦 ∈ ran 𝐴 ↔ ∃ 𝑥 𝑥 𝐴 𝑦 )
3 2 biimpi ⊢ ( 𝑦 ∈ ran 𝐴 → ∃ 𝑥 𝑥 𝐴 𝑦 )
4 3 biantrurd ⊢ ( 𝑦 ∈ ran 𝐴 → ( ∃* 𝑥 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) ) )
5 4 ralbiia ⊢ ( ∀ 𝑦 ∈ ran 𝐴 ∃* 𝑥 𝑥 𝐴 𝑦 ↔ ∀ 𝑦 ∈ ran 𝐴 ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) )
6 funcnv ⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∈ ran 𝐴 ∃* 𝑥 𝑥 𝐴 𝑦 )
7 df-reu ⊢ ( ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 ↔ ∃! 𝑥 ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
8 vex ⊢ 𝑥 ∈ V
9 vex ⊢ 𝑦 ∈ V
10 8 9 breldm ⊢ ( 𝑥 𝐴 𝑦 → 𝑥 ∈ dom 𝐴 )
11 10 pm4.71ri ⊢ ( 𝑥 𝐴 𝑦 ↔ ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
12 11 eubii ⊢ ( ∃! 𝑥 𝑥 𝐴 𝑦 ↔ ∃! 𝑥 ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
13 df-eu ⊢ ( ∃! 𝑥 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) )
14 7 12 13 3bitr2i ⊢ ( ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) )
15 14 ralbii ⊢ ( ∀ 𝑦 ∈ ran 𝐴 ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 ↔ ∀ 𝑦 ∈ ran 𝐴 ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) )
16 5 6 15 3bitr4i ⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∈ ran 𝐴 ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 )