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

Metamath Proof Explorer

Theorem dffun2

Description: Alternate definition of a function. (Contributed by NM, 29-Dec-1996) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

Ref Expression
Assertion dffun2 ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 df-fun ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) )
2 cotrg ⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) )
3 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑤 ◡ 𝐴 𝑥 ) )
4 3 anbi1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ↔ ( 𝑤 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ) )
5 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 I 𝑧 ↔ 𝑤 I 𝑧 ) )
6 4 5 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ( ( 𝑤 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑤 I 𝑧 ) ) )
7 6 albidv ⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑧 ( ( 𝑤 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑤 I 𝑧 ) ) )
8 breq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑦 ◡ 𝐴 𝑤 ) )
9 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝐴 𝑧 ↔ 𝑤 𝐴 𝑧 ) )
10 8 9 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ↔ ( 𝑦 ◡ 𝐴 𝑤 ∧ 𝑤 𝐴 𝑧 ) ) )
11 10 imbi1d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ( ( 𝑦 ◡ 𝐴 𝑤 ∧ 𝑤 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ) )
12 11 albidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑤 ∧ 𝑤 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ) )
13 7 12 alcomw ⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) )
14 vex ⊢ 𝑦 ∈ V
15 vex ⊢ 𝑥 ∈ V
16 14 15 brcnv ⊢ ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑦 )
17 16 anbi1i ⊢ ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) )
18 vex ⊢ 𝑧 ∈ V
19 18 ideq ⊢ ( 𝑦 I 𝑧 ↔ 𝑦 = 𝑧 )
20 17 19 imbi12i ⊢ ( ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
21 20 3albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
22 13 21 bitri ⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
23 2 22 bitri ⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
24 23 anbi2i ⊢ ( ( Rel 𝐴 ∧ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )
25 1 24 bitri ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )