Metamath Proof Explorer


Theorem 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 𝐹 = ( 𝑥𝐴 , 𝑦𝐵 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
Assertion xpsff1o 𝐹 : ( 𝐴 × 𝐵 ) –1-1-ontoX 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 )

Proof

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