Metamath Proof Explorer


Theorem ixpsnf1o

Description: A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypothesis ixpsnf1o.f 𝐹 = ( 𝑥𝐴 ↦ ( { 𝐼 } × { 𝑥 } ) )
Assertion ixpsnf1o ( 𝐼𝑉𝐹 : 𝐴1-1-ontoX 𝑦 ∈ { 𝐼 } 𝐴 )

Proof

Step Hyp Ref Expression
1 ixpsnf1o.f 𝐹 = ( 𝑥𝐴 ↦ ( { 𝐼 } × { 𝑥 } ) )
2 snex { 𝐼 } ∈ V
3 snex { 𝑥 } ∈ V
4 2 3 xpex ( { 𝐼 } × { 𝑥 } ) ∈ V
5 4 a1i ( ( 𝐼𝑉𝑥𝐴 ) → ( { 𝐼 } × { 𝑥 } ) ∈ V )
6 vex 𝑎 ∈ V
7 6 rnex ran 𝑎 ∈ V
8 7 uniex ran 𝑎 ∈ V
9 8 a1i ( ( 𝐼𝑉𝑎X 𝑦 ∈ { 𝐼 } 𝐴 ) → ran 𝑎 ∈ V )
10 sneq ( 𝑏 = 𝐼 → { 𝑏 } = { 𝐼 } )
11 10 xpeq1d ( 𝑏 = 𝐼 → ( { 𝑏 } × { 𝑥 } ) = ( { 𝐼 } × { 𝑥 } ) )
12 11 eqeq2d ( 𝑏 = 𝐼 → ( 𝑎 = ( { 𝑏 } × { 𝑥 } ) ↔ 𝑎 = ( { 𝐼 } × { 𝑥 } ) ) )
13 12 anbi2d ( 𝑏 = 𝐼 → ( ( 𝑥𝐴𝑎 = ( { 𝑏 } × { 𝑥 } ) ) ↔ ( 𝑥𝐴𝑎 = ( { 𝐼 } × { 𝑥 } ) ) ) )
14 elixpsn ( 𝑏 ∈ V → ( 𝑎X 𝑦 ∈ { 𝑏 } 𝐴 ↔ ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
15 14 elv ( 𝑎X 𝑦 ∈ { 𝑏 } 𝐴 ↔ ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } )
16 10 ixpeq1d ( 𝑏 = 𝐼X 𝑦 ∈ { 𝑏 } 𝐴 = X 𝑦 ∈ { 𝐼 } 𝐴 )
17 16 eleq2d ( 𝑏 = 𝐼 → ( 𝑎X 𝑦 ∈ { 𝑏 } 𝐴𝑎X 𝑦 ∈ { 𝐼 } 𝐴 ) )
18 15 17 bitr3id ( 𝑏 = 𝐼 → ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ↔ 𝑎X 𝑦 ∈ { 𝐼 } 𝐴 ) )
19 18 anbi1d ( 𝑏 = 𝐼 → ( ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran 𝑎 ) ↔ ( 𝑎X 𝑦 ∈ { 𝐼 } 𝐴𝑥 = ran 𝑎 ) ) )
20 vex 𝑏 ∈ V
21 vex 𝑥 ∈ V
22 20 21 xpsn ( { 𝑏 } × { 𝑥 } ) = { ⟨ 𝑏 , 𝑥 ⟩ }
23 22 eqeq2i ( 𝑎 = ( { 𝑏 } × { 𝑥 } ) ↔ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } )
24 23 anbi2i ( ( 𝑥𝐴𝑎 = ( { 𝑏 } × { 𝑥 } ) ) ↔ ( 𝑥𝐴𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) )
25 eqid { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ }
26 opeq2 ( 𝑐 = 𝑥 → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝑏 , 𝑥 ⟩ )
27 26 sneqd ( 𝑐 = 𝑥 → { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } )
28 27 rspceeqv ( ( 𝑥𝐴 ∧ { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) → ∃ 𝑐𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } )
29 25 28 mpan2 ( 𝑥𝐴 → ∃ 𝑐𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } )
30 20 21 op2nda ran { ⟨ 𝑏 , 𝑥 ⟩ } = 𝑥
31 30 eqcomi 𝑥 = ran { ⟨ 𝑏 , 𝑥 ⟩ }
32 29 31 jctir ( 𝑥𝐴 → ( ∃ 𝑐𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran { ⟨ 𝑏 , 𝑥 ⟩ } ) )
33 eqeq1 ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ↔ { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
34 33 rexbidv ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ↔ ∃ 𝑐𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
35 rneq ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ran 𝑎 = ran { ⟨ 𝑏 , 𝑥 ⟩ } )
36 35 unieqd ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ran 𝑎 = ran { ⟨ 𝑏 , 𝑥 ⟩ } )
37 36 eqeq2d ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( 𝑥 = ran 𝑎𝑥 = ran { ⟨ 𝑏 , 𝑥 ⟩ } ) )
38 34 37 anbi12d ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran 𝑎 ) ↔ ( ∃ 𝑐𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
39 32 38 syl5ibrcom ( 𝑥𝐴 → ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran 𝑎 ) ) )
40 39 imp ( ( 𝑥𝐴𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) → ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran 𝑎 ) )
41 vex 𝑐 ∈ V
42 20 41 op2nda ran { ⟨ 𝑏 , 𝑐 ⟩ } = 𝑐
43 42 eqeq2i ( 𝑥 = ran { ⟨ 𝑏 , 𝑐 ⟩ } ↔ 𝑥 = 𝑐 )
44 eqidd ( 𝑐𝐴 → { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } )
45 44 ancli ( 𝑐𝐴 → ( 𝑐𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
46 eleq1w ( 𝑥 = 𝑐 → ( 𝑥𝐴𝑐𝐴 ) )
47 opeq2 ( 𝑥 = 𝑐 → ⟨ 𝑏 , 𝑥 ⟩ = ⟨ 𝑏 , 𝑐 ⟩ )
48 47 sneqd ( 𝑥 = 𝑐 → { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } )
49 48 eqeq2d ( 𝑥 = 𝑐 → ( { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ↔ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
50 46 49 anbi12d ( 𝑥 = 𝑐 → ( ( 𝑥𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ↔ ( 𝑐𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) ) )
51 45 50 syl5ibrcom ( 𝑐𝐴 → ( 𝑥 = 𝑐 → ( 𝑥𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
52 43 51 syl5bi ( 𝑐𝐴 → ( 𝑥 = ran { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
53 rneq ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ran 𝑎 = ran { ⟨ 𝑏 , 𝑐 ⟩ } )
54 53 unieqd ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ran 𝑎 = ran { ⟨ 𝑏 , 𝑐 ⟩ } )
55 54 eqeq2d ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥 = ran 𝑎𝑥 = ran { ⟨ 𝑏 , 𝑐 ⟩ } ) )
56 eqeq1 ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ↔ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) )
57 56 anbi2d ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( ( 𝑥𝐴𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ↔ ( 𝑥𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
58 55 57 imbi12d ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( ( 𝑥 = ran 𝑎 → ( 𝑥𝐴𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) ↔ ( 𝑥 = ran { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) ) )
59 52 58 syl5ibrcom ( 𝑐𝐴 → ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥 = ran 𝑎 → ( 𝑥𝐴𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) ) )
60 59 rexlimiv ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥 = ran 𝑎 → ( 𝑥𝐴𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
61 60 imp ( ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran 𝑎 ) → ( 𝑥𝐴𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) )
62 40 61 impbii ( ( 𝑥𝐴𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ↔ ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran 𝑎 ) )
63 24 62 bitri ( ( 𝑥𝐴𝑎 = ( { 𝑏 } × { 𝑥 } ) ) ↔ ( ∃ 𝑐𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ran 𝑎 ) )
64 13 19 63 vtoclbg ( 𝐼𝑉 → ( ( 𝑥𝐴𝑎 = ( { 𝐼 } × { 𝑥 } ) ) ↔ ( 𝑎X 𝑦 ∈ { 𝐼 } 𝐴𝑥 = ran 𝑎 ) ) )
65 1 5 9 64 f1od ( 𝐼𝑉𝐹 : 𝐴1-1-ontoX 𝑦 ∈ { 𝐼 } 𝐴 )