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

Metamath Proof Explorer

Theorem f1ompt

Description: Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015) (Revised by Mario Carneiro, 4-Dec-2016)

Ref Expression
Hypothesis fmpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
Assertion f1ompt ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fmpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
3 dff1o4 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )
4 3 baib ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ◡ 𝐹 Fn 𝐵 ) )
5 2 4 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ◡ 𝐹 Fn 𝐵 ) )
6 fnres ⊢ ( ( ◡ 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑧 𝑦 ◡ 𝐹 𝑧 )
7 nfcv ⊢ Ⅎ 𝑥 𝑧
8 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
9 1 8 nfcxfr ⊢ Ⅎ 𝑥 𝐹
10 nfcv ⊢ Ⅎ 𝑥 𝑦
11 7 9 10 nfbr ⊢ Ⅎ 𝑥 𝑧 𝐹 𝑦
12 nfv ⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 )
13 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐹 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
14 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
15 1 14 eqtri ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
16 15 breqi ⊢ ( 𝑥 𝐹 𝑦 ↔ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } 𝑦 )
17 df-br ⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } )
18 opabidw ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) )
19 17 18 bitri ⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) )
20 16 19 bitri ⊢ ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) )
21 13 20 bitrdi ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) )
22 11 12 21 cbveuw ⊢ ( ∃! 𝑧 𝑧 𝐹 𝑦 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) )
23 vex ⊢ 𝑦 ∈ V
24 vex ⊢ 𝑧 ∈ V
25 23 24 brcnv ⊢ ( 𝑦 ◡ 𝐹 𝑧 ↔ 𝑧 𝐹 𝑦 )
26 25 eubii ⊢ ( ∃! 𝑧 𝑦 ◡ 𝐹 𝑧 ↔ ∃! 𝑧 𝑧 𝐹 𝑦 )
27 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) )
28 22 26 27 3bitr4i ⊢ ( ∃! 𝑧 𝑦 ◡ 𝐹 𝑧 ↔ ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
29 28 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃! 𝑧 𝑦 ◡ 𝐹 𝑧 ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
30 6 29 bitri ⊢ ( ( ◡ 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
31 relcnv ⊢ Rel ◡ 𝐹
32 df-rn ⊢ ran 𝐹 = dom ◡ 𝐹
33 frn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran 𝐹 ⊆ 𝐵 )
34 32 33 eqsstrrid ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom ◡ 𝐹 ⊆ 𝐵 )
35 relssres ⊢ ( ( Rel ◡ 𝐹 ∧ dom ◡ 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 ↾ 𝐵 ) = ◡ 𝐹 )
36 31 34 35 sylancr ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐹 ↾ 𝐵 ) = ◡ 𝐹 )
37 36 fneq1d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( ◡ 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ ◡ 𝐹 Fn 𝐵 ) )
38 30 37 bitr3id ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ◡ 𝐹 Fn 𝐵 ) )
39 5 38 bitr4d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
40 39 pm5.32i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
41 f1of ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
42 41 pm4.71ri ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
43 1 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
44 43 anbi1i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
45 40 42 44 3bitr4i ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )