Metamath Proof Explorer

Theorem f1mpt

Description: Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses f1mpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
f1mpt.2 ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
Assertion f1mpt ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 f1mpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2 f1mpt.2 ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
3 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
4 1 3 nfcxfr ⊢ Ⅎ 𝑥 𝐹
5 nfcv ⊢ Ⅎ 𝑦 𝐹
6 4 5 dff13f ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
7 1 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
8 7 anbi1i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
9 2 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐶 ∈ 𝐵 ↔ 𝐷 ∈ 𝐵 ) )
10 9 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝐷 ∈ 𝐵 )
11 raaanv ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐴 𝐷 ∈ 𝐵 ) )
12 1 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
13 2 1 fvmptg ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = 𝐷 )
14 12 13 eqeqan12d ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝐶 = 𝐷 ) )
15 14 an4s ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝐶 = 𝐷 ) )
16 15 imbi1d ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
17 16 ex ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) ) )
18 17 ralimdva ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) ) )
19 ralbi ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
20 18 19 syl6 ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) ) )
21 20 ralimia ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
22 ralbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
23 21 22 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
24 11 23 sylbir ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐴 𝐷 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
25 10 24 sylan2b ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
26 25 anidms ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
27 26 pm5.32i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )
28 6 8 27 3bitr2i ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) )