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 𝑥𝐴 𝐶ontoX 𝑥𝐵 𝐶 )

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 syl5bi ( 𝐵𝐴 → ( X 𝑥𝐴 𝐶 ≠ ∅ → ∀ X 𝑥𝐵 𝐶𝑦X 𝑥𝐴 𝐶 = ( 𝐹𝑦 ) ) )
61 60 imp ( ( 𝐵𝐴X 𝑥𝐴 𝐶 ≠ ∅ ) → ∀ X 𝑥𝐵 𝐶𝑦X 𝑥𝐴 𝐶 = ( 𝐹𝑦 ) )
62 dffo3 ( 𝐹 : X 𝑥𝐴 𝐶ontoX 𝑥𝐵 𝐶 ↔ ( 𝐹 : X 𝑥𝐴 𝐶X 𝑥𝐵 𝐶 ∧ ∀ X 𝑥𝐵 𝐶𝑦X 𝑥𝐴 𝐶 = ( 𝐹𝑦 ) ) )
63 4 61 62 sylanbrc ( ( 𝐵𝐴X 𝑥𝐴 𝐶 ≠ ∅ ) → 𝐹 : X 𝑥𝐴 𝐶ontoX 𝑥𝐵 𝐶 )