Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem pw2en 3348

Description: The power set of a set is equinumerous to set exponentiation with a base of ordinal 2. Proposition 10.44 of [TakeutiZaring] p. 96. (This proof seems excessively long. An attempt to find a shorter one is on my to-do list.)

**Hypothesis**
Ref	Expression
pw2en.1	⊢ A ∈ V

**Assertion**
Ref	Expression
pw2en	⊢ ℘A ≈ (2_o ↑_m A)

**Proof of Theorem pw2en**
Step	Hyp	Ref	Expression
1		pw2en.1	. . 3 ⊢ A ∈ V
2	1	pwex 1806	. 2 ⊢ ℘A ∈ V
3		moeq 1431	. . . . 5 ⊢ ∃*w w = {v∣(v = ∅ ∧ z ∈ x)}
4	3	a1i 7	. . . 4 ⊢ (z ∈ A → ∃*w w = {v∣(v = ∅ ∧ z ∈ x)})
5	1, 4	funopabex 2742	. . 3 ⊢ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ∈ V
6	5	a1i 7	. 2 ⊢ (x ∈ ℘A → {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ∈ V)
7		visset 1350	. . . . 5 ⊢ y ∈ V
8	7	cnvex 2670	. . . 4 ⊢ ^◡y ∈ V
9		imaexg 2612	. . . 4 ⊢ (^◡y ∈ V → (^◡y “ {{∅}}) ∈ V)
10	8, 9	ax-mp 6	. . 3 ⊢ (^◡y “ {{∅}}) ∈ V
11	10	a1i 7	. 2 ⊢ (y ∈ (2_o ↑_m A) → (^◡y “ {{∅}}) ∈ V)
12		sseqin2 1656	. . . . . . . . . 10 ⊢ (x ⊆ A ↔ (A ∩ x) = x)
13	12	biimp 133	. . . . . . . . 9 ⊢ (x ⊆ A → (A ∩ x) = x)
14	13	cleq1d 1109	. . . . . . . 8 ⊢ (x ⊆ A → ((A ∩ x) = (^◡y “ {{∅}}) ↔ x = (^◡y “ {{∅}})))
15		eleq2 1150	. . . . . . . . . . 11 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (⟨u, {∅}⟩ ∈ y ↔ ⟨u, {∅}⟩ ∈ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}))
16		p0ex 1885	. . . . . . . . . . . . 13 ⊢ {∅} ∈ V
17		visset 1350	. . . . . . . . . . . . 13 ⊢ u ∈ V
18	16, 17	elimasn 2617	. . . . . . . . . . . 12 ⊢ (u ∈ (^◡y “ {{∅}}) ↔ ⟨{∅}, u⟩ ∈ ^◡y)
19	16, 17	opelcnv 2518	. . . . . . . . . . . 12 ⊢ (⟨{∅}, u⟩ ∈ ^◡y ↔ ⟨u, {∅}⟩ ∈ y)
20	18, 19	bitr 151	. . . . . . . . . . 11 ⊢ (u ∈ (^◡y “ {{∅}}) ↔ ⟨u, {∅}⟩ ∈ y)
21	15, 20	syl5bb 410	. . . . . . . . . 10 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (u ∈ (^◡y “ {{∅}}) ↔ ⟨u, {∅}⟩ ∈ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}))
22		cleq2ab 1179	. . . . . . . . . . . . 13 ⊢ ({v∣v = ∅} = {v∣(v = ∅ ∧ u ∈ x)} ↔ ∀v(v = ∅ ↔ (v = ∅ ∧ u ∈ x)))
23		df-sn 1811	. . . . . . . . . . . . . 14 ⊢ {∅} = {v∣v = ∅}
24	23	cleq1i 1108	. . . . . . . . . . . . 13 ⊢ ({∅} = {v∣(v = ∅ ∧ u ∈ x)} ↔ {v∣v = ∅} = {v∣(v = ∅ ∧ u ∈ x)})
25		iba 486	. . . . . . . . . . . . . . 15 ⊢ (u ∈ x → (v = ∅ ↔ (v = ∅ ∧ u ∈ x)))
26	25	19.21aiv 943	. . . . . . . . . . . . . 14 ⊢ (u ∈ x → ∀v(v = ∅ ↔ (v = ∅ ∧ u ∈ x)))
27		0ex 1745	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ V
28		cleq1 1107	. . . . . . . . . . . . . . . . 17 ⊢ (v = ∅ → (v = ∅ ↔ ∅ = ∅))
29	28	anbi1d 469	. . . . . . . . . . . . . . . . 17 ⊢ (v = ∅ → ((v = ∅ ∧ u ∈ x) ↔ (∅ = ∅ ∧ u ∈ x)))
30	28, 29	bibi12d 477	. . . . . . . . . . . . . . . 16 ⊢ (v = ∅ → ((v = ∅ ↔ (v = ∅ ∧ u ∈ x)) ↔ (∅ = ∅ ↔ (∅ = ∅ ∧ u ∈ x))))
31	27, 30	cla4v 1400	. . . . . . . . . . . . . . 15 ⊢ (∀v(v = ∅ ↔ (v = ∅ ∧ u ∈ x)) → (∅ = ∅ ↔ (∅ = ∅ ∧ u ∈ x)))
32		cleqid 1102	. . . . . . . . . . . . . . . . 17 ⊢ ∅ = ∅
33	32	a1bi 172	. . . . . . . . . . . . . . . 16 ⊢ (u ∈ x ↔ (∅ = ∅ → u ∈ x))
34		pm4.71 481	. . . . . . . . . . . . . . . 16 ⊢ ((∅ = ∅ → u ∈ x) ↔ (∅ = ∅ ↔ (∅ = ∅ ∧ u ∈ x)))
35	33, 34	bitr 151	. . . . . . . . . . . . . . 15 ⊢ (u ∈ x ↔ (∅ = ∅ ↔ (∅ = ∅ ∧ u ∈ x)))
36	31, 35	sylibr 175	. . . . . . . . . . . . . 14 ⊢ (∀v(v = ∅ ↔ (v = ∅ ∧ u ∈ x)) → u ∈ x)
37	26, 36	impbi 139	. . . . . . . . . . . . 13 ⊢ (u ∈ x ↔ ∀v(v = ∅ ↔ (v = ∅ ∧ u ∈ x)))
38	22, 24, 37	3bitr4r 159	. . . . . . . . . . . 12 ⊢ (u ∈ x ↔ {∅} = {v∣(v = ∅ ∧ u ∈ x)})
39	38	anbi2i 367	. . . . . . . . . . 11 ⊢ ((u ∈ A ∧ u ∈ x) ↔ (u ∈ A ∧ {∅} = {v∣(v = ∅ ∧ u ∈ x)}))
40		elin 1635	. . . . . . . . . . 11 ⊢ (u ∈ (A ∩ x) ↔ (u ∈ A ∧ u ∈ x))
41		eleq1 1149	. . . . . . . . . . . . 13 ⊢ (z = u → (z ∈ A ↔ u ∈ A))
42		eleq1 1149	. . . . . . . . . . . . . . . 16 ⊢ (z = u → (z ∈ x ↔ u ∈ x))
43	42	anbi2d 468	. . . . . . . . . . . . . . 15 ⊢ (z = u → ((v = ∅ ∧ z ∈ x) ↔ (v = ∅ ∧ u ∈ x)))
44	43	biabdv 1183	. . . . . . . . . . . . . 14 ⊢ (z = u → {v∣(v = ∅ ∧ z ∈ x)} = {v∣(v = ∅ ∧ u ∈ x)})
45	44	cleq2d 1112	. . . . . . . . . . . . 13 ⊢ (z = u → (w = {v∣(v = ∅ ∧ z ∈ x)} ↔ w = {v∣(v = ∅ ∧ u ∈ x)}))
46	41, 45	anbi12d 476	. . . . . . . . . . . 12 ⊢ (z = u → ((z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)}) ↔ (u ∈ A ∧ w = {v∣(v = ∅ ∧ u ∈ x)})))
47		cleq1 1107	. . . . . . . . . . . . 13 ⊢ (w = {∅} → (w = {v∣(v = ∅ ∧ u ∈ x)} ↔ {∅} = {v∣(v = ∅ ∧ u ∈ x)}))
48	47	anbi2d 468	. . . . . . . . . . . 12 ⊢ (w = {∅} → ((u ∈ A ∧ w = {v∣(v = ∅ ∧ u ∈ x)}) ↔ (u ∈ A ∧ {∅} = {v∣(v = ∅ ∧ u ∈ x)})))
49	17, 16, 46, 48	opelopab 2117	. . . . . . . . . . 11 ⊢ (⟨u, {∅}⟩ ∈ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ↔ (u ∈ A ∧ {∅} = {v∣(v = ∅ ∧ u ∈ x)}))
50	39, 40, 49	3bitr4 158	. . . . . . . . . 10 ⊢ (u ∈ (A ∩ x) ↔ ⟨u, {∅}⟩ ∈ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})})
51	21, 50	syl6rbbr 417	. . . . . . . . 9 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (u ∈ (A ∩ x) ↔ u ∈ (^◡y “ {{∅}})))
52	51	cleqrd 1100	. . . . . . . 8 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (A ∩ x) = (^◡y “ {{∅}}))
53	14, 52	syl5bi 183	. . . . . . 7 ⊢ (x ⊆ A → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → x = (^◡y “ {{∅}})))
54	53	com12 13	. . . . . 6 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (x ⊆ A → x = (^◡y “ {{∅}})))
55		sseq1 1521	. . . . . . . 8 ⊢ (x = (^◡y “ {{∅}}) → (x ⊆ A ↔ (^◡y “ {{∅}}) ⊆ A))
56		imassrn 2611	. . . . . . . . 9 ⊢ (^◡y “ {{∅}}) ⊆ ran ^◡y
57	23, 16	eqeltrr 1160	. . . . . . . . . . . . . . 15 ⊢ {v∣v = ∅} ∈ V
58		pm3.26 256	. . . . . . . . . . . . . . . 16 ⊢ ((v = ∅ ∧ z ∈ x) → v = ∅)
59	58	ss2abi 1552	. . . . . . . . . . . . . . 15 ⊢ {v∣(v = ∅ ∧ z ∈ x)} ⊆ {v∣v = ∅}
60	57, 59	ssexi 1701	. . . . . . . . . . . . . 14 ⊢ {v∣(v = ∅ ∧ z ∈ x)} ∈ V
61		cleqid 1102	. . . . . . . . . . . . . 14 ⊢ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}
62	60, 61	fnopab2 2747	. . . . . . . . . . . . 13 ⊢ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} Fn A
63		fneq1 2718	. . . . . . . . . . . . 13 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (y Fn A ↔ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} Fn A))
64	62, 63	mpbiri 169	. . . . . . . . . . . 12 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → y Fn A)
65		fndm 2723	. . . . . . . . . . . 12 ⊢ (y Fn A → dom y = A)
66	64, 65	syl 12	. . . . . . . . . . 11 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → dom y = A)
67		dfdm4 2525	. . . . . . . . . . 11 ⊢ dom y = ran ^◡y
68	66, 67	syl5eqr 1138	. . . . . . . . . 10 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → ran ^◡y = A)
69	68	sseq2d 1528	. . . . . . . . 9 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → ((^◡y “ {{∅}}) ⊆ ran ^◡y ↔ (^◡y “ {{∅}}) ⊆ A))
70	56, 69	mpbii 168	. . . . . . . 8 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (^◡y “ {{∅}}) ⊆ A)
71	55, 70	syl5bir 184	. . . . . . 7 ⊢ (x = (^◡y “ {{∅}}) → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → x ⊆ A))
72	71	com12 13	. . . . . 6 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (x = (^◡y “ {{∅}}) → x ⊆ A))
73	54, 72	impbid 397	. . . . 5 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (x ⊆ A ↔ x = (^◡y “ {{∅}})))
74		visset 1350	. . . . . 6 ⊢ x ∈ V
75	74	elpw 1801	. . . . 5 ⊢ (x ∈ ℘A ↔ x ⊆ A)
76	73, 75	syl5bb 410	. . . 4 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (x ∈ ℘A ↔ x = (^◡y “ {{∅}})))
77	76	pm5.32ri 490	. . 3 ⊢ ((x ∈ ℘A ∧ y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}) ↔ (x = (^◡y “ {{∅}}) ∧ y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}))
78		ancom 333	. . 3 ⊢ ((x = (^◡y “ {{∅}}) ∧ y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}) ↔ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ∧ x = (^◡y “ {{∅}})))
79	16	pri2 1842	. . . . . . . . . . . . . 14 ⊢ {∅} ∈ {∅, {∅}}
80		df2o2 3112	. . . . . . . . . . . . . 14 ⊢ 2_o = {∅, {∅}}
81	79, 80	eleqtrr 1162	. . . . . . . . . . . . 13 ⊢ {∅} ∈ 2_o
82		iba 486	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ x → (v = ∅ ↔ (v = ∅ ∧ z ∈ x)))
83		elsn 1820	. . . . . . . . . . . . . . . 16 ⊢ (v ∈ {∅} ↔ v = ∅)
84	82, 83	syl5bb 410	. . . . . . . . . . . . . . 15 ⊢ (z ∈ x → (v ∈ {∅} ↔ (v = ∅ ∧ z ∈ x)))
85	84	biabrdv 1184	. . . . . . . . . . . . . 14 ⊢ (z ∈ x → {∅} = {v∣(v = ∅ ∧ z ∈ x)})
86	85	eleq1d 1155	. . . . . . . . . . . . 13 ⊢ (z ∈ x → ({∅} ∈ 2_o ↔ {v∣(v = ∅ ∧ z ∈ x)} ∈ 2_o))
87	81, 86	mpbii 168	. . . . . . . . . . . 12 ⊢ (z ∈ x → {v∣(v = ∅ ∧ z ∈ x)} ∈ 2_o)
88	27	pri1 1841	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ {∅, {∅}}
89	88, 80	eleqtrr 1162	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 2_o
90		abn0 1715	. . . . . . . . . . . . . . . 16 ⊢ (¬ {v∣(v = ∅ ∧ z ∈ x)} = ∅ ↔ ∃v(v = ∅ ∧ z ∈ x))
91		pm3.27 260	. . . . . . . . . . . . . . . . 17 ⊢ ((v = ∅ ∧ z ∈ x) → z ∈ x)
92	91	19.23aiv 952	. . . . . . . . . . . . . . . 16 ⊢ (∃v(v = ∅ ∧ z ∈ x) → z ∈ x)
93	90, 92	sylbi 174	. . . . . . . . . . . . . . 15 ⊢ (¬ {v∣(v = ∅ ∧ z ∈ x)} = ∅ → z ∈ x)
94	93	con1i 88	. . . . . . . . . . . . . 14 ⊢ (¬ z ∈ x → {v∣(v = ∅ ∧ z ∈ x)} = ∅)
95	94	eleq1d 1155	. . . . . . . . . . . . 13 ⊢ (¬ z ∈ x → ({v∣(v = ∅ ∧ z ∈ x)} ∈ 2_o ↔ ∅ ∈ 2_o))
96	89, 95	mpbiri 169	. . . . . . . . . . . 12 ⊢ (¬ z ∈ x → {v∣(v = ∅ ∧ z ∈ x)} ∈ 2_o)
97	87, 96	pm2.61i 110	. . . . . . . . . . 11 ⊢ {v∣(v = ∅ ∧ z ∈ x)} ∈ 2_o
98	97	a1i 7	. . . . . . . . . 10 ⊢ (z ∈ A → {v∣(v = ∅ ∧ z ∈ x)} ∈ 2_o)
99	98	rgen 1247	. . . . . . . . 9 ⊢ ∀z ∈ A {v∣(v = ∅ ∧ z ∈ x)} ∈ 2_o
100	61	fopab2 2891	. . . . . . . . 9 ⊢ (∀z ∈ A {v∣(v = ∅ ∧ z ∈ x)} ∈ 2_o ↔ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}:A–→2_o)
101	99, 100	mpbi 164	. . . . . . . 8 ⊢ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}:A–→2_o
102		feq1 2748	. . . . . . . 8 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → (y:A–→2_o ↔ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}:A–→2_o))
103	101, 102	mpbiri 169	. . . . . . 7 ⊢ (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → y:A–→2_o)
104	103	a1i 7	. . . . . 6 ⊢ (x = (^◡y “ {{∅}}) → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → y:A–→2_o))
105		eleq2 1150	. . . . . . . . . . . . . . . . 17 ⊢ (x = (^◡y “ {{∅}}) → (z ∈ x ↔ z ∈ (^◡y “ {{∅}})))
106		visset 1350	. . . . . . . . . . . . . . . . . . 19 ⊢ z ∈ V
107	16, 106	elimasn 2617	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ (^◡y “ {{∅}}) ↔ ⟨{∅}, z⟩ ∈ ^◡y)
108	16, 106	opelcnv 2518	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨{∅}, z⟩ ∈ ^◡y ↔ ⟨z, {∅}⟩ ∈ y)
109	107, 108	bitr 151	. . . . . . . . . . . . . . . . 17 ⊢ (z ∈ (^◡y “ {{∅}}) ↔ ⟨z, {∅}⟩ ∈ y)
110	105, 109	syl6bb 414	. . . . . . . . . . . . . . . 16 ⊢ (x = (^◡y “ {{∅}}) → (z ∈ x ↔ ⟨z, {∅}⟩ ∈ y))
111	16	fnfvop 2856	. . . . . . . . . . . . . . . . . 18 ⊢ ((y Fn A ∧ z ∈ A) → ((y ‘z) = {∅} ↔ ⟨z, {∅}⟩ ∈ y))
112		ffn 2752	. . . . . . . . . . . . . . . . . 18 ⊢ (y:A–→2_o → y Fn A)
113	111, 112	sylan 343	. . . . . . . . . . . . . . . . 17 ⊢ ((y:A–→2_o ∧ z ∈ A) → ((y ‘z) = {∅} ↔ ⟨z, {∅}⟩ ∈ y))
114	113	bicomd 399	. . . . . . . . . . . . . . . 16 ⊢ ((y:A–→2_o ∧ z ∈ A) → (⟨z, {∅}⟩ ∈ y ↔ (y ‘z) = {∅}))
115	110, 114	sylan9bb 418	. . . . . . . . . . . . . . 15 ⊢ ((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) → (z ∈ x ↔ (y ‘z) = {∅}))
116	115	biimpa 324	. . . . . . . . . . . . . 14 ⊢ (((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) ∧ z ∈ x) → (y ‘z) = {∅})
117	85	adantl 305	. . . . . . . . . . . . . 14 ⊢ (((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) ∧ z ∈ x) → {∅} = {v∣(v = ∅ ∧ z ∈ x)})
118	116, 117	eqtrd 1128	. . . . . . . . . . . . 13 ⊢ (((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) ∧ z ∈ x) → (y ‘z) = {v∣(v = ∅ ∧ z ∈ x)})
119		ffvrn 2890	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y:A–→2_o ∧ z ∈ A) → (y ‘z) ∈ 2_o)
120	80	eleq2i 1153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ‘z) ∈ 2_o ↔ (y ‘z) ∈ {∅, {∅}})
121		fvex 2838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ‘z) ∈ V
122	121	elpr 1823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ‘z) ∈ {∅, {∅}} ↔ ((y ‘z) = ∅ ∨ (y ‘z) = {∅}))
123	120, 122	bitr 151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ‘z) ∈ 2_o ↔ ((y ‘z) = ∅ ∨ (y ‘z) = {∅}))
124	119, 123	sylib 173	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y:A–→2_o ∧ z ∈ A) → ((y ‘z) = ∅ ∨ (y ‘z) = {∅}))
125	124	ord 202	. . . . . . . . . . . . . . . . . 18 ⊢ ((y:A–→2_o ∧ z ∈ A) → (¬ (y ‘z) = ∅ → (y ‘z) = {∅}))
126	125	adantl 305	. . . . . . . . . . . . . . . . 17 ⊢ ((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) → (¬ (y ‘z) = ∅ → (y ‘z) = {∅}))
127	126, 115	sylibrd 179	. . . . . . . . . . . . . . . 16 ⊢ ((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) → (¬ (y ‘z) = ∅ → z ∈ x))
128	127	con1d 85	. . . . . . . . . . . . . . 15 ⊢ ((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) → (¬ z ∈ x → (y ‘z) = ∅))
129	128	imp 277	. . . . . . . . . . . . . 14 ⊢ (((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) ∧ ¬ z ∈ x) → (y ‘z) = ∅)
130	94	adantl 305	. . . . . . . . . . . . . 14 ⊢ (((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) ∧ ¬ z ∈ x) → {v∣(v = ∅ ∧ z ∈ x)} = ∅)
131	129, 130	eqtr4d 1131	. . . . . . . . . . . . 13 ⊢ (((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) ∧ ¬ z ∈ x) → (y ‘z) = {v∣(v = ∅ ∧ z ∈ x)})
132	118, 131	pm2.61an2 365	. . . . . . . . . . . 12 ⊢ ((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) → (y ‘z) = {v∣(v = ∅ ∧ z ∈ x)})
133		fvopab2 2878	. . . . . . . . . . . . . 14 ⊢ ((z ∈ A ∧ {v∣(v = ∅ ∧ z ∈ x)} ∈ V) → ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z) = {v∣(v = ∅ ∧ z ∈ x)})
134	60, 133	mpan2 519	. . . . . . . . . . . . 13 ⊢ (z ∈ A → ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z) = {v∣(v = ∅ ∧ z ∈ x)})
135	134	ad2antrr 323	. . . . . . . . . . . 12 ⊢ ((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) → ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z) = {v∣(v = ∅ ∧ z ∈ x)})
136	132, 135	eqtr4d 1131	. . . . . . . . . . 11 ⊢ ((x = (^◡y “ {{∅}}) ∧ (y:A–→2_o ∧ z ∈ A)) → (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z))
137	136	exp32 294	. . . . . . . . . 10 ⊢ (x = (^◡y “ {{∅}}) → (y:A–→2_o → (z ∈ A → (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z))))
138	137	imp 277	. . . . . . . . 9 ⊢ ((x = (^◡y “ {{∅}}) ∧ y:A–→2_o) → (z ∈ A → (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z)))
139	138	r19.21aiv 1259	. . . . . . . 8 ⊢ ((x = (^◡y “ {{∅}}) ∧ y:A–→2_o) → ∀z ∈ A (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z))
140		ax-17 925	. . . . . . . . . . . . 13 ⊢ (u ∈ y → ∀z u ∈ y)
141		hbopab1 2112	. . . . . . . . . . . . 13 ⊢ (u ∈ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} → ∀z u ∈ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})})
142	140, 141	cleqfvf 2881	. . . . . . . . . . . 12 ⊢ ((y Fn A ∧ {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} Fn A) → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ↔ (A = A ∧ ∀z ∈ A (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z))))
143	62, 142	mpan2 519	. . . . . . . . . . 11 ⊢ (y Fn A → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ↔ (A = A ∧ ∀z ∈ A (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z))))
144		cleqid 1102	. . . . . . . . . . . 12 ⊢ A = A
145	144	biantrur 544	. . . . . . . . . . 11 ⊢ (∀z ∈ A (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z) ↔ (A = A ∧ ∀z ∈ A (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z)))
146	143, 145	syl6bbr 416	. . . . . . . . . 10 ⊢ (y Fn A → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ↔ ∀z ∈ A (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z)))
147	112, 146	syl 12	. . . . . . . . 9 ⊢ (y:A–→2_o → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ↔ ∀z ∈ A (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z)))
148	147	adantl 305	. . . . . . . 8 ⊢ ((x = (^◡y “ {{∅}}) ∧ y:A–→2_o) → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ↔ ∀z ∈ A (y ‘z) = ({⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ‘z)))
149	139, 148	mpbird 171	. . . . . . 7 ⊢ ((x = (^◡y “ {{∅}}) ∧ y:A–→2_o) → y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})})
150	149	exp 291	. . . . . 6 ⊢ (x = (^◡y “ {{∅}}) → (y:A–→2_o → y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}))
151	104, 150	impbid 397	. . . . 5 ⊢ (x = (^◡y “ {{∅}}) → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ↔ y:A–→2_o))
152		2o 3110	. . . . . . 7 ⊢ 2_o ∈ On
153	152	elisseti 1355	. . . . . 6 ⊢ 2_o ∈ V
154	153, 1	elmap 3265	. . . . 5 ⊢ (y ∈ (2_o ↑_m A) ↔ y:A–→2_o)
155	151, 154	syl6bbr 416	. . . 4 ⊢ (x = (^◡y “ {{∅}}) → (y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ↔ y ∈ (2_o ↑_m A)))
156	155	pm5.32ri 490	. . 3 ⊢ ((y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})} ∧ x = (^◡y “ {{∅}})) ↔ (y ∈ (2_o ↑_m A) ∧ x = (^◡y “ {{∅}})))
157	77, 78, 156	3bitr 155	. 2 ⊢ ((x ∈ ℘A ∧ y = {⟨z, w⟩∣(z ∈ A ∧ w = {v∣(v = ∅ ∧ z ∈ x)})}) ↔ (y ∈ (2_o ↑_m A) ∧ x = (^◡y “ {{∅}})))
158	2, 6, 11, 157	en2 3305	1 ⊢ ℘A ≈ (2_o ↑_m A)

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 ∀wal 672 ∃wex 678 = weq 797 ∈ wel 803 ∃*wmo 1008 {cab 1090 = wceq 1091 ∈ wcel 1092 ∀wral 1201 Vcvv 1348 ∩ cin 1486 ⊆ wss 1487 ∅c0 1707 ℘cpw 1798 {csn 1808 {cpr 1809 ⟨cop 1810 class class class wbr 2054 {copab 2055 Oncon0 2199 ^◡ccnv 2409 dom cdm 2410 ran crn 2411 “ cima 2413 Fn wfn 2417 –→wf 2418 ‘cfv 2422 (class class class)co 3001 2_oc2o 3100 ↑_m cm 3258 ≈ cen 3271

This theorem is referenced by: pwen 3398 aleph1 3676 infmap1 4950

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-suc 2205 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-opr 3003 df-oprab 3004 df-1o 3104 df-2o 3105 df-map 3259 df-en 3274

metamath.org