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

Metamath Proof Explorer

Theorem f1ocnvd

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

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

Proof

Step Hyp Ref Expression
1 f1od.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2 f1od.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 )
3 f1od.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝑋 )
4 f1od.4 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) )
5 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝑊 )
6 1 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝑊 → 𝐹 Fn 𝐴 )
7 5 6 syl ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
8 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 𝐷 ∈ 𝑋 )
9 eqid ⊢ ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) = ( 𝑦 ∈ 𝐵 ↦ 𝐷 )
10 9 fnmpt ⊢ ( ∀ 𝑦 ∈ 𝐵 𝐷 ∈ 𝑋 → ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 )
11 8 10 syl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 )
12 4 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) } )
13 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
14 1 13 eqtri ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
15 14 cnveqi ⊢ ◡ 𝐹 = ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
16 cnvopab ⊢ ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
17 15 16 eqtri ⊢ ◡ 𝐹 = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
18 df-mpt ⊢ ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) }
19 12 17 18 3eqtr4g ⊢ ( 𝜑 → ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) )
20 19 fneq1d ⊢ ( 𝜑 → ( ◡ 𝐹 Fn 𝐵 ↔ ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 ) )
21 11 20 mpbird ⊢ ( 𝜑 → ◡ 𝐹 Fn 𝐵 )
22 dff1o4 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )
23 7 21 22 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
24 23 19 jca ⊢ ( 𝜑 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) ) )