This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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-onto→ X 𝑦 ∈ { 𝐼 } 𝐴 )

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 biimtrid ⊢ ( 𝑐 ∈ 𝐴 → ( 𝑥 = ∪ 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-onto→ X 𝑦 ∈ { 𝐼 } 𝐴 )