This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ↦ ( 𝑓 ↾ 𝐵 ) )
Assertion resixpfo ( ( 𝐵 ⊆ 𝐴 ∧ X 𝑥 ∈ 𝐴 𝐶 ≠ ∅ ) → 𝐹 : X 𝑥 ∈ 𝐴 𝐶 –onto→ X 𝑥 ∈ 𝐵 𝐶 )

Proof

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