Metamath Proof Explorer

Theorem f1oresf1o2

Description: Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022)

Ref Expression
Hypotheses f1oresf1o2.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
f1oresf1o2.2 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
f1oresf1o2.3 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐷 ↔ 𝜒 ) )
Assertion f1oresf1o2 ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )

Proof

Step Hyp Ref Expression
1 f1oresf1o2.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
2 f1oresf1o2.2 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
3 f1oresf1o2.3 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐷 ↔ 𝜒 ) )
4 f1of ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
5 1 4 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
7 2 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐴 )
8 6 7 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
9 8 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
10 ffvelrn ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
11 9 10 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
12 eleq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
13 12 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
14 11 13 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐵 )
15 eqcom ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) )
16 3 biimpd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐷 → 𝜒 ) )
17 16 ex ⊢ ( 𝜑 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑥 ∈ 𝐷 → 𝜒 ) ) )
18 15 17 syl5bi ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝑥 ∈ 𝐷 → 𝜒 ) ) )
19 18 com23 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝜒 ) ) )
20 19 3imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝜒 )
21 14 20 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝑦 ∈ 𝐵 ∧ 𝜒 ) )
22 21 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝑦 ∈ 𝐵 ∧ 𝜒 ) ) )
23 f1ofo ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
24 1 23 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 –onto→ 𝐵 )
25 foelrni ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
26 24 25 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
27 26 ex ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
28 nfv ⊢ Ⅎ 𝑥 𝜑
29 nfv ⊢ Ⅎ 𝑥 𝜒
30 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦
31 29 30 nfim ⊢ Ⅎ 𝑥 ( 𝜒 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
32 rspe ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
33 32 expcom ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝑥 ∈ 𝐷 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
34 33 eqcoms ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑥 ∈ 𝐷 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐷 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
36 3 35 sylbird ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝜒 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
37 36 ex ⊢ ( 𝜑 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝜒 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝜒 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
39 15 38 syl5bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝜒 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
40 39 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝜒 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) ) )
41 28 31 40 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝜒 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
42 27 41 syld ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝜒 → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
43 42 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ∧ 𝜒 ) → ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
44 22 43 impbid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜒 ) ) )
45 1 2 44 f1oresf1o ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )