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 ⊢ F = x ∈ A ⟼ I × x
Assertion ixpsnf1o ⊢ I ∈ V → F : A ⟶ 1-1 onto ⨉ y ∈ I A

Proof

Step Hyp Ref Expression
1 ixpsnf1o.f ⊢ F = x ∈ A ⟼ I × x
2 snex ⊢ I ∈ V
3 snex ⊢ x ∈ V
4 2 3 xpex ⊢ I × x ∈ V
5 4 a1i ⊢ I ∈ V ∧ x ∈ A → I × x ∈ V
6 vex ⊢ a ∈ V
7 6 rnex ⊢ ran ⁡ a ∈ V
8 7 uniex ⊢ ⋃ ran ⁡ a ∈ V
9 8 a1i ⊢ I ∈ V ∧ a ∈ ⨉ y ∈ I A → ⋃ ran ⁡ a ∈ V
10 sneq ⊢ b = I → b = I
11 10 xpeq1d ⊢ b = I → b × x = I × x
12 11 eqeq2d ⊢ b = I → a = b × x ↔ a = I × x
13 12 anbi2d ⊢ b = I → x ∈ A ∧ a = b × x ↔ x ∈ A ∧ a = I × x
14 elixpsn ⊢ b ∈ V → a ∈ ⨉ y ∈ b A ↔ ∃ c ∈ A a = b c
15 14 elv ⊢ a ∈ ⨉ y ∈ b A ↔ ∃ c ∈ A a = b c
16 10 ixpeq1d ⊢ b = I → ⨉ y ∈ b A = ⨉ y ∈ I A
17 16 eleq2d ⊢ b = I → a ∈ ⨉ y ∈ b A ↔ a ∈ ⨉ y ∈ I A
18 15 17 bitr3id ⊢ b = I → ∃ c ∈ A a = b c ↔ a ∈ ⨉ y ∈ I A
19 18 anbi1d ⊢ b = I → ∃ c ∈ A a = b c ∧ x = ⋃ ran ⁡ a ↔ a ∈ ⨉ y ∈ I A ∧ x = ⋃ ran ⁡ a
20 vex ⊢ b ∈ V
21 vex ⊢ x ∈ V
22 20 21 xpsn ⊢ b × x = b x
23 22 eqeq2i ⊢ a = b × x ↔ a = b x
24 23 anbi2i ⊢ x ∈ A ∧ a = b × x ↔ x ∈ A ∧ a = b x
25 eqid ⊢ b x = b x
26 opeq2 ⊢ c = x → b c = b x
27 26 sneqd ⊢ c = x → b c = b x
28 27 rspceeqv ⊢ x ∈ A ∧ b x = b x → ∃ c ∈ A b x = b c
29 25 28 mpan2 ⊢ x ∈ A → ∃ c ∈ A b x = b c
30 20 21 op2nda ⊢ ⋃ ran ⁡ b x = x
31 30 eqcomi ⊢ x = ⋃ ran ⁡ b x
32 29 31 jctir ⊢ x ∈ A → ∃ c ∈ A b x = b c ∧ x = ⋃ ran ⁡ b x
33 eqeq1 ⊢ a = b x → a = b c ↔ b x = b c
34 33 rexbidv ⊢ a = b x → ∃ c ∈ A a = b c ↔ ∃ c ∈ A b x = b c
35 rneq ⊢ a = b x → ran ⁡ a = ran ⁡ b x
36 35 unieqd ⊢ a = b x → ⋃ ran ⁡ a = ⋃ ran ⁡ b x
37 36 eqeq2d ⊢ a = b x → x = ⋃ ran ⁡ a ↔ x = ⋃ ran ⁡ b x
38 34 37 anbi12d ⊢ a = b x → ∃ c ∈ A a = b c ∧ x = ⋃ ran ⁡ a ↔ ∃ c ∈ A b x = b c ∧ x = ⋃ ran ⁡ b x
39 32 38 syl5ibrcom ⊢ x ∈ A → a = b x → ∃ c ∈ A a = b c ∧ x = ⋃ ran ⁡ a
40 39 imp ⊢ x ∈ A ∧ a = b x → ∃ c ∈ A a = b c ∧ x = ⋃ ran ⁡ a
41 vex ⊢ c ∈ V
42 20 41 op2nda ⊢ ⋃ ran ⁡ b c = c
43 42 eqeq2i ⊢ x = ⋃ ran ⁡ b c ↔ x = c
44 eqidd ⊢ c ∈ A → b c = b c
45 44 ancli ⊢ c ∈ A → c ∈ A ∧ b c = b c
46 eleq1w ⊢ x = c → x ∈ A ↔ c ∈ A
47 opeq2 ⊢ x = c → b x = b c
48 47 sneqd ⊢ x = c → b x = b c
49 48 eqeq2d ⊢ x = c → b c = b x ↔ b c = b c
50 46 49 anbi12d ⊢ x = c → x ∈ A ∧ b c = b x ↔ c ∈ A ∧ b c = b c
51 45 50 syl5ibrcom ⊢ c ∈ A → x = c → x ∈ A ∧ b c = b x
52 43 51 syl5bi ⊢ c ∈ A → x = ⋃ ran ⁡ b c → x ∈ A ∧ b c = b x
53 rneq ⊢ a = b c → ran ⁡ a = ran ⁡ b c
54 53 unieqd ⊢ a = b c → ⋃ ran ⁡ a = ⋃ ran ⁡ b c
55 54 eqeq2d ⊢ a = b c → x = ⋃ ran ⁡ a ↔ x = ⋃ ran ⁡ b c
56 eqeq1 ⊢ a = b c → a = b x ↔ b c = b x
57 56 anbi2d ⊢ a = b c → x ∈ A ∧ a = b x ↔ x ∈ A ∧ b c = b x
58 55 57 imbi12d ⊢ a = b c → x = ⋃ ran ⁡ a → x ∈ A ∧ a = b x ↔ x = ⋃ ran ⁡ b c → x ∈ A ∧ b c = b x
59 52 58 syl5ibrcom ⊢ c ∈ A → a = b c → x = ⋃ ran ⁡ a → x ∈ A ∧ a = b x
60 59 rexlimiv ⊢ ∃ c ∈ A a = b c → x = ⋃ ran ⁡ a → x ∈ A ∧ a = b x
61 60 imp ⊢ ∃ c ∈ A a = b c ∧ x = ⋃ ran ⁡ a → x ∈ A ∧ a = b x
62 40 61 impbii ⊢ x ∈ A ∧ a = b x ↔ ∃ c ∈ A a = b c ∧ x = ⋃ ran ⁡ a
63 24 62 bitri ⊢ x ∈ A ∧ a = b × x ↔ ∃ c ∈ A a = b c ∧ x = ⋃ ran ⁡ a
64 13 19 63 vtoclbg ⊢ I ∈ V → x ∈ A ∧ a = I × x ↔ a ∈ ⨉ y ∈ I A ∧ x = ⋃ ran ⁡ a
65 1 5 9 64 f1od ⊢ I ∈ V → F : A ⟶ 1-1 onto ⨉ y ∈ I A