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

Metamath Proof Explorer

Theorem f1ocnv2d

Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses f1od.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
f1o2d.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
f1o2d.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝐴 )
f1o2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
Assertion f1ocnv2d ( 𝜑 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 f1od.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2 f1o2d.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
3 f1o2d.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝐴 )
4 f1o2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
5 eleq1a ⊢ ( 𝐶 ∈ 𝐵 → ( 𝑦 = 𝐶 → 𝑦 ∈ 𝐵 ) )
6 2 5 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = 𝐶 → 𝑦 ∈ 𝐵 ) )
7 6 impr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → 𝑦 ∈ 𝐵 )
8 4 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝐷 )
9 8 exp42 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝑦 = 𝐶 → 𝑥 = 𝐷 ) ) ) )
10 9 com34 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐶 → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝐷 ) ) ) )
11 10 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝐷 ) )
12 7 11 jcai ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) )
13 eleq1a ⊢ ( 𝐷 ∈ 𝐴 → ( 𝑥 = 𝐷 → 𝑥 ∈ 𝐴 ) )
14 3 13 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐷 → 𝑥 ∈ 𝐴 ) )
15 14 impr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → 𝑥 ∈ 𝐴 )
16 4 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑥 = 𝐷 ) → 𝑦 = 𝐶 )
17 16 exp42 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝑥 = 𝐷 → 𝑦 = 𝐶 ) ) ) )
18 17 com23 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝐷 → 𝑦 = 𝐶 ) ) ) )
19 18 com34 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝑥 = 𝐷 → ( 𝑥 ∈ 𝐴 → 𝑦 = 𝐶 ) ) ) )
20 19 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → ( 𝑥 ∈ 𝐴 → 𝑦 = 𝐶 ) )
21 15 20 jcai ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) )
22 12 21 impbida ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) )
23 1 2 3 22 f1ocnvd ⊢ ( 𝜑 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) ) )