Metamath Proof Explorer

Theorem resixpfo

Description: Restriction of elements of an infinite Cartesian product creates a surjection, if the original Cartesian product is nonempty. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis resixpfo.1 ⊢ F = f ∈ ⨉ x ∈ A C ⟼ f ↾ B
Assertion resixpfo ⊢ B ⊆ A ∧ ⨉ x ∈ A C ≠ ∅ → F : ⨉ x ∈ A C ⟶ onto ⨉ x ∈ B C

Proof

Step Hyp Ref Expression
1 resixpfo.1 ⊢ F = f ∈ ⨉ x ∈ A C ⟼ f ↾ B
2 resixp ⊢ B ⊆ A ∧ f ∈ ⨉ x ∈ A C → f ↾ B ∈ ⨉ x ∈ B C
3 2 1 fmptd ⊢ B ⊆ A → F : ⨉ x ∈ A C ⟶ ⨉ x ∈ B C
4 3 adantr ⊢ B ⊆ A ∧ ⨉ x ∈ A C ≠ ∅ → F : ⨉ x ∈ A C ⟶ ⨉ x ∈ B C
5 n0 ⊢ ⨉ x ∈ A C ≠ ∅ ↔ ∃ g g ∈ ⨉ x ∈ A C
6 eleq1w ⊢ z = x → z ∈ B ↔ x ∈ B
7 6 ifbid ⊢ z = x → if z ∈ B h g = if x ∈ B h g
8 id ⊢ z = x → z = x
9 7 8 fveq12d ⊢ z = x → if z ∈ B h g ⁡ z = if x ∈ B h g ⁡ x
10 9 cbvmptv ⊢ z ∈ A ⟼ if z ∈ B h g ⁡ z = x ∈ A ⟼ if x ∈ B h g ⁡ x
11 vex ⊢ h ∈ V
12 11 elixp ⊢ h ∈ ⨉ x ∈ B C ↔ h Fn B ∧ ∀ x ∈ B h ⁡ x ∈ C
13 12 simprbi ⊢ h ∈ ⨉ x ∈ B C → ∀ x ∈ B h ⁡ x ∈ C
14 fveq1 ⊢ h = if x ∈ B h g → h ⁡ x = if x ∈ B h g ⁡ x
15 14 eleq1d ⊢ h = if x ∈ B h g → h ⁡ x ∈ C ↔ if x ∈ B h g ⁡ x ∈ C
16 fveq1 ⊢ g = if x ∈ B h g → g ⁡ x = if x ∈ B h g ⁡ x
17 16 eleq1d ⊢ g = if x ∈ B h g → g ⁡ x ∈ C ↔ if x ∈ B h g ⁡ x ∈ C
18 simpl ⊢ x ∈ B → h ⁡ x ∈ C ∧ x ∈ A ∧ g ⁡ x ∈ C → x ∈ B → h ⁡ x ∈ C
19 18 imp ⊢ x ∈ B → h ⁡ x ∈ C ∧ x ∈ A ∧ g ⁡ x ∈ C ∧ x ∈ B → h ⁡ x ∈ C
20 simplrr ⊢ x ∈ B → h ⁡ x ∈ C ∧ x ∈ A ∧ g ⁡ x ∈ C ∧ ¬ x ∈ B → g ⁡ x ∈ C
21 15 17 19 20 ifbothda ⊢ x ∈ B → h ⁡ x ∈ C ∧ x ∈ A ∧ g ⁡ x ∈ C → if x ∈ B h g ⁡ x ∈ C
22 21 exp32 ⊢ x ∈ B → h ⁡ x ∈ C → x ∈ A → g ⁡ x ∈ C → if x ∈ B h g ⁡ x ∈ C
23 22 ralimi2 ⊢ ∀ x ∈ B h ⁡ x ∈ C → ∀ x ∈ A g ⁡ x ∈ C → if x ∈ B h g ⁡ x ∈ C
24 13 23 syl ⊢ h ∈ ⨉ x ∈ B C → ∀ x ∈ A g ⁡ x ∈ C → if x ∈ B h g ⁡ x ∈ C
25 24 adantl ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C → ∀ x ∈ A g ⁡ x ∈ C → if x ∈ B h g ⁡ x ∈ C
26 ralim ⊢ ∀ x ∈ A g ⁡ x ∈ C → if x ∈ B h g ⁡ x ∈ C → ∀ x ∈ A g ⁡ x ∈ C → ∀ x ∈ A if x ∈ B h g ⁡ x ∈ C
27 25 26 syl ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C → ∀ x ∈ A g ⁡ x ∈ C → ∀ x ∈ A if x ∈ B h g ⁡ x ∈ C
28 vex ⊢ g ∈ V
29 28 elixp ⊢ g ∈ ⨉ x ∈ A C ↔ g Fn A ∧ ∀ x ∈ A g ⁡ x ∈ C
30 29 simprbi ⊢ g ∈ ⨉ x ∈ A C → ∀ x ∈ A g ⁡ x ∈ C
31 27 30 impel ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → ∀ x ∈ A if x ∈ B h g ⁡ x ∈ C
32 n0i ⊢ g ∈ ⨉ x ∈ A C → ¬ ⨉ x ∈ A C = ∅
33 ixpprc ⊢ ¬ A ∈ V → ⨉ x ∈ A C = ∅
34 32 33 nsyl2 ⊢ g ∈ ⨉ x ∈ A C → A ∈ V
35 34 adantl ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → A ∈ V
36 mptelixpg ⊢ A ∈ V → x ∈ A ⟼ if x ∈ B h g ⁡ x ∈ ⨉ x ∈ A C ↔ ∀ x ∈ A if x ∈ B h g ⁡ x ∈ C
37 35 36 syl ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → x ∈ A ⟼ if x ∈ B h g ⁡ x ∈ ⨉ x ∈ A C ↔ ∀ x ∈ A if x ∈ B h g ⁡ x ∈ C
38 31 37 mpbird ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → x ∈ A ⟼ if x ∈ B h g ⁡ x ∈ ⨉ x ∈ A C
39 10 38 eqeltrid ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → z ∈ A ⟼ if z ∈ B h g ⁡ z ∈ ⨉ x ∈ A C
40 reseq1 ⊢ f = z ∈ A ⟼ if z ∈ B h g ⁡ z → f ↾ B = z ∈ A ⟼ if z ∈ B h g ⁡ z ↾ B
41 iftrue ⊢ z ∈ B → if z ∈ B h g = h
42 41 fveq1d ⊢ z ∈ B → if z ∈ B h g ⁡ z = h ⁡ z
43 42 mpteq2ia ⊢ z ∈ B ⟼ if z ∈ B h g ⁡ z = z ∈ B ⟼ h ⁡ z
44 resmpt ⊢ B ⊆ A → z ∈ A ⟼ if z ∈ B h g ⁡ z ↾ B = z ∈ B ⟼ if z ∈ B h g ⁡ z
45 44 ad2antrr ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → z ∈ A ⟼ if z ∈ B h g ⁡ z ↾ B = z ∈ B ⟼ if z ∈ B h g ⁡ z
46 ixpfn ⊢ h ∈ ⨉ x ∈ B C → h Fn B
47 46 ad2antlr ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → h Fn B
48 dffn5 ⊢ h Fn B ↔ h = z ∈ B ⟼ h ⁡ z
49 47 48 sylib ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → h = z ∈ B ⟼ h ⁡ z
50 43 45 49 3eqtr4a ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → z ∈ A ⟼ if z ∈ B h g ⁡ z ↾ B = h
51 50 11 eqeltrdi ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → z ∈ A ⟼ if z ∈ B h g ⁡ z ↾ B ∈ V
52 1 40 39 51 fvmptd3 ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → F ⁡ z ∈ A ⟼ if z ∈ B h g ⁡ z = z ∈ A ⟼ if z ∈ B h g ⁡ z ↾ B
53 52 50 eqtr2d ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → h = F ⁡ z ∈ A ⟼ if z ∈ B h g ⁡ z
54 fveq2 ⊢ y = z ∈ A ⟼ if z ∈ B h g ⁡ z → F ⁡ y = F ⁡ z ∈ A ⟼ if z ∈ B h g ⁡ z
55 54 rspceeqv ⊢ z ∈ A ⟼ if z ∈ B h g ⁡ z ∈ ⨉ x ∈ A C ∧ h = F ⁡ z ∈ A ⟼ if z ∈ B h g ⁡ z → ∃ y ∈ ⨉ x ∈ A C h = F ⁡ y
56 39 53 55 syl2anc ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C ∧ g ∈ ⨉ x ∈ A C → ∃ y ∈ ⨉ x ∈ A C h = F ⁡ y
57 56 ex ⊢ B ⊆ A ∧ h ∈ ⨉ x ∈ B C → g ∈ ⨉ x ∈ A C → ∃ y ∈ ⨉ x ∈ A C h = F ⁡ y
58 57 ralrimdva ⊢ B ⊆ A → g ∈ ⨉ x ∈ A C → ∀ h ∈ ⨉ x ∈ B C ∃ y ∈ ⨉ x ∈ A C h = F ⁡ y
59 58 exlimdv ⊢ B ⊆ A → ∃ g g ∈ ⨉ x ∈ A C → ∀ h ∈ ⨉ x ∈ B C ∃ y ∈ ⨉ x ∈ A C h = F ⁡ y
60 5 59 syl5bi ⊢ B ⊆ A → ⨉ x ∈ A C ≠ ∅ → ∀ h ∈ ⨉ x ∈ B C ∃ y ∈ ⨉ x ∈ A C h = F ⁡ y
61 60 imp ⊢ B ⊆ A ∧ ⨉ x ∈ A C ≠ ∅ → ∀ h ∈ ⨉ x ∈ B C ∃ y ∈ ⨉ x ∈ A C h = F ⁡ y
62 dffo3 ⊢ F : ⨉ x ∈ A C ⟶ onto ⨉ x ∈ B C ↔ F : ⨉ x ∈ A C ⟶ ⨉ x ∈ B C ∧ ∀ h ∈ ⨉ x ∈ B C ∃ y ∈ ⨉ x ∈ A C h = F ⁡ y
63 4 61 62 sylanbrc ⊢ B ⊆ A ∧ ⨉ x ∈ A C ≠ ∅ → F : ⨉ x ∈ A C ⟶ onto ⨉ x ∈ B C