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𝐵 ↔ ( ∀ 𝑥𝐴 𝐶𝐵 ∧ ∀ 𝑦𝐵 ∃! 𝑥𝐴 𝑦 = 𝐶 ) )