xpsff1o

Description: The function appearing in xpsval is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o } . (Contributed by Mario Carneiro, 15-Aug-2015)

		Ref	Expression
	Hypothesis	xpsff1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
	Assertion	xpsff1o	⊢ 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		xpsff1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
2		xpsfrnel2	⊢ ( { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3	2	biimpri	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) )
4	3	rgen2	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 )
5	1	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ 𝐹 : ( 𝐴 × 𝐵 ) ⟶ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) )
6	4 5	mpbi	⊢ 𝐹 : ( 𝐴 × 𝐵 ) ⟶ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 )
7		1st2nd2	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
8	7	fveq2d	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
9		df-ov	⊢ ( ( 1^st ‘ 𝑧 ) 𝐹 ( 2^nd ‘ 𝑧 ) ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
10		xp1st	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 1^st ‘ 𝑧 ) ∈ 𝐴 )
11		xp2nd	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 2^nd ‘ 𝑧 ) ∈ 𝐵 )
12	1	xpsfval	⊢ ( ( ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ( ( 1^st ‘ 𝑧 ) 𝐹 ( 2^nd ‘ 𝑧 ) ) = { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } )
13	10 11 12	syl2anc	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( ( 1^st ‘ 𝑧 ) 𝐹 ( 2^nd ‘ 𝑧 ) ) = { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } )
14	9 13	eqtr3id	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) = { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } )
15	8 14	eqtrd	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } )
16		1st2nd2	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
17	16	fveq2d	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
18		df-ov	⊢ ( ( 1^st ‘ 𝑤 ) 𝐹 ( 2^nd ‘ 𝑤 ) ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
19		xp1st	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 1^st ‘ 𝑤 ) ∈ 𝐴 )
20		xp2nd	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 2^nd ‘ 𝑤 ) ∈ 𝐵 )
21	1	xpsfval	⊢ ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐵 ) → ( ( 1^st ‘ 𝑤 ) 𝐹 ( 2^nd ‘ 𝑤 ) ) = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } )
22	19 20 21	syl2anc	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( ( 1^st ‘ 𝑤 ) 𝐹 ( 2^nd ‘ 𝑤 ) ) = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } )
23	18 22	eqtr3id	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } )
24	17 23	eqtrd	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 𝐹 ‘ 𝑤 ) = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } )
25	15 24	eqeqan12d	⊢ ( ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } ) )
26		fveq1	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } → ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } ‘ ∅ ) = ( { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ ∅ ) )
27		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
28		fvpr0o	⊢ ( ( 1^st ‘ 𝑧 ) ∈ V → ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } ‘ ∅ ) = ( 1^st ‘ 𝑧 ) )
29	27 28	ax-mp	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } ‘ ∅ ) = ( 1^st ‘ 𝑧 )
30		fvex	⊢ ( 1^st ‘ 𝑤 ) ∈ V
31		fvpr0o	⊢ ( ( 1^st ‘ 𝑤 ) ∈ V → ( { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ ∅ ) = ( 1^st ‘ 𝑤 ) )
32	30 31	ax-mp	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ ∅ ) = ( 1^st ‘ 𝑤 )
33	26 29 32	3eqtr3g	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } → ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑤 ) )
34		fveq1	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } → ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } ‘ 1_o ) = ( { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ 1_o ) )
35		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
36		fvpr1o	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ V → ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } ‘ 1_o ) = ( 2^nd ‘ 𝑧 ) )
37	35 36	ax-mp	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } ‘ 1_o ) = ( 2^nd ‘ 𝑧 )
38		fvex	⊢ ( 2^nd ‘ 𝑤 ) ∈ V
39		fvpr1o	⊢ ( ( 2^nd ‘ 𝑤 ) ∈ V → ( { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ 1_o ) = ( 2^nd ‘ 𝑤 ) )
40	38 39	ax-mp	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ 1_o ) = ( 2^nd ‘ 𝑤 )
41	34 37 40	3eqtr3g	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } → ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑤 ) )
42	33 41	opeq12d	⊢ ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } → ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
43	7 16	eqeqan12d	⊢ ( ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) → ( 𝑧 = 𝑤 ↔ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
44	42 43	imbitrrid	⊢ ( ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) → ( { ⟨ ∅ , ( 1^st ‘ 𝑧 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑧 ) ⟩ } = { ⟨ ∅ , ( 1^st ‘ 𝑤 ) ⟩ , ⟨ 1_o , ( 2^nd ‘ 𝑤 ) ⟩ } → 𝑧 = 𝑤 ) )
45	25 44	sylbid	⊢ ( ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
46	45	rgen2	⊢ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 )
47		dff13	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
48	6 46 47	mpbir2an	⊢ 𝐹 : ( 𝐴 × 𝐵 ) –1-1→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 )
49		xpsfrnel	⊢ ( 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝑧 Fn 2_o ∧ ( 𝑧 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝑧 ‘ 1_o ) ∈ 𝐵 ) )
50	49	simp2bi	⊢ ( 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → ( 𝑧 ‘ ∅ ) ∈ 𝐴 )
51	49	simp3bi	⊢ ( 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → ( 𝑧 ‘ 1_o ) ∈ 𝐵 )
52	1	xpsfval	⊢ ( ( ( 𝑧 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝑧 ‘ 1_o ) ∈ 𝐵 ) → ( ( 𝑧 ‘ ∅ ) 𝐹 ( 𝑧 ‘ 1_o ) ) = { ⟨ ∅ , ( 𝑧 ‘ ∅ ) ⟩ , ⟨ 1_o , ( 𝑧 ‘ 1_o ) ⟩ } )
53	50 51 52	syl2anc	⊢ ( 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → ( ( 𝑧 ‘ ∅ ) 𝐹 ( 𝑧 ‘ 1_o ) ) = { ⟨ ∅ , ( 𝑧 ‘ ∅ ) ⟩ , ⟨ 1_o , ( 𝑧 ‘ 1_o ) ⟩ } )
54		ixpfn	⊢ ( 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → 𝑧 Fn 2_o )
55		xpsfeq	⊢ ( 𝑧 Fn 2_o → { ⟨ ∅ , ( 𝑧 ‘ ∅ ) ⟩ , ⟨ 1_o , ( 𝑧 ‘ 1_o ) ⟩ } = 𝑧 )
56	54 55	syl	⊢ ( 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → { ⟨ ∅ , ( 𝑧 ‘ ∅ ) ⟩ , ⟨ 1_o , ( 𝑧 ‘ 1_o ) ⟩ } = 𝑧 )
57	53 56	eqtr2d	⊢ ( 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → 𝑧 = ( ( 𝑧 ‘ ∅ ) 𝐹 ( 𝑧 ‘ 1_o ) ) )
58		rspceov	⊢ ( ( ( 𝑧 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝑧 ‘ 1_o ) ∈ 𝐵 ∧ 𝑧 = ( ( 𝑧 ‘ ∅ ) 𝐹 ( 𝑧 ‘ 1_o ) ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 𝐹 𝑏 ) )
59	50 51 57 58	syl3anc	⊢ ( 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 𝐹 𝑏 ) )
60	59	rgen	⊢ ∀ 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 𝐹 𝑏 )
61		foov	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –onto→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ∧ ∀ 𝑧 ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 𝐹 𝑏 ) ) )
62	6 60 61	mpbir2an	⊢ 𝐹 : ( 𝐴 × 𝐵 ) –onto→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 )
63		df-f1o	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ∧ 𝐹 : ( 𝐴 × 𝐵 ) –onto→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) )
64	48 62 63	mpbir2an	⊢ 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 )

Metamath Proof Explorer

Theorem xpsff1o

Proof