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