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