dfac12r

Description: The axiom of choice holds iff every ordinal has a well-orderable powerset. This version of dfac12 does not assume the Axiom of Regularity. (Contributed by Mario Carneiro, 29-May-2015)

		Ref	Expression
	Assertion	dfac12r	$⊢ \forall x \in On 𝒫 x \in dom card \leftrightarrow ⋃ R_{1} [On] \subseteq dom card$

Proof

Step	Hyp	Ref	Expression
1		rankwflemb	$⊢ y \in ⋃ R_{1} [On] \leftrightarrow \exists z \in On y \in R_{1} (suc z)$
2		harcl	$⊢ har (R_{1} (z)) \in On$
3		pweq	$⊢ x = har (R_{1} (z)) \to 𝒫 x = 𝒫 har (R_{1} (z))$
4	3	eleq1d	$⊢ x = har (R_{1} (z)) \to (𝒫 x \in dom card \leftrightarrow 𝒫 har (R_{1} (z)) \in dom card)$
5	4	rspcv	$⊢ har (R_{1} (z)) \in On \to (\forall x \in On 𝒫 x \in dom card \to 𝒫 har (R_{1} (z)) \in dom card)$
6	2 5	ax-mp	$⊢ \forall x \in On 𝒫 x \in dom card \to 𝒫 har (R_{1} (z)) \in dom card$
7		cardid2	$⊢ 𝒫 har (R_{1} (z)) \in dom card \to card (𝒫 har (R_{1} (z))) \approx 𝒫 har (R_{1} (z))$
8		ensym	$⊢ card (𝒫 har (R_{1} (z))) \approx 𝒫 har (R_{1} (z)) \to 𝒫 har (R_{1} (z)) \approx card (𝒫 har (R_{1} (z)))$
9		bren	$⊢ 𝒫 har (R_{1} (z)) \approx card (𝒫 har (R_{1} (z))) \leftrightarrow \exists f f : 𝒫 har (R_{1} (z)) \underset{1-1 onto}{⟶} card (𝒫 har (R_{1} (z)))$
10		simpr	$⊢ (f : 𝒫 har (R_{1} (z)) \underset{1-1 onto}{⟶} card (𝒫 har (R_{1} (z))) \land z \in On) \to z \in On$
11		f1of1	$⊢ f : 𝒫 har (R_{1} (z)) \underset{1-1 onto}{⟶} card (𝒫 har (R_{1} (z))) \to f : 𝒫 har (R_{1} (z)) \underset{1-1}{⟶} card (𝒫 har (R_{1} (z)))$
12	11	adantr	$⊢ (f : 𝒫 har (R_{1} (z)) \underset{1-1 onto}{⟶} card (𝒫 har (R_{1} (z))) \land z \in On) \to f : 𝒫 har (R_{1} (z)) \underset{1-1}{⟶} card (𝒫 har (R_{1} (z)))$
13		cardon	$⊢ card (𝒫 har (R_{1} (z))) \in On$
14	13	onssi	$⊢ card (𝒫 har (R_{1} (z))) \subseteq On$
15		f1ss	$⊢ (f : 𝒫 har (R_{1} (z)) \underset{1-1}{⟶} card (𝒫 har (R_{1} (z))) \land card (𝒫 har (R_{1} (z))) \subseteq On) \to f : 𝒫 har (R_{1} (z)) \underset{1-1}{⟶} On$
16	12 14 15	sylancl	$⊢ (f : 𝒫 har (R_{1} (z)) \underset{1-1 onto}{⟶} card (𝒫 har (R_{1} (z))) \land z \in On) \to f : 𝒫 har (R_{1} (z)) \underset{1-1}{⟶} On$
17		fveq2	$⊢ y = b \to rank (y) = rank (b)$
18	17	oveq2d	$⊢ y = b \to suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y) = suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (b)$
19		suceq	$⊢ rank (y) = rank (b) \to suc rank (y) = suc rank (b)$
20	17 19	syl	$⊢ y = b \to suc rank (y) = suc rank (b)$
21	20	fveq2d	$⊢ y = b \to x (suc rank (y)) = x (suc rank (b))$
22		id	$⊢ y = b \to y = b$
23	21 22	fveq12d	$⊢ y = b \to x (suc rank (y)) (y) = x (suc rank (b)) (b)$
24	18 23	oveq12d	$⊢ y = b \to (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y) = (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (b)) +_{𝑜} x (suc rank (b)) (b)$
25		imaeq2	$⊢ y = b \to ({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y] = ({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [b]$
26	25	fveq2d	$⊢ y = b \to f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y]) = f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [b])$
27	24 26	ifeq12d	$⊢ y = b \to if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y])) = if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (b)) +_{𝑜} x (suc rank (b)) (b), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [b]))$
28	27	cbvmptv	$⊢ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y]))) = (b \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (b)) +_{𝑜} x (suc rank (b)) (b), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [b])))$
29		dmeq	$⊢ x = a \to dom x = dom a$
30	29	fveq2d	$⊢ x = a \to R_{1} (dom x) = R_{1} (dom a)$
31	29	unieqd	$⊢ x = a \to ⋃ dom x = ⋃ dom a$
32	29 31	eqeq12d	$⊢ x = a \to (dom x = ⋃ dom x \leftrightarrow dom a = ⋃ dom a)$
33		rneq	$⊢ x = a \to ran x = ran a$
34	33	unieqd	$⊢ x = a \to ⋃ ran x = ⋃ ran a$
35	34	rneqd	$⊢ x = a \to ran ⋃ ran x = ran ⋃ ran a$
36	35	unieqd	$⊢ x = a \to ⋃ ran ⋃ ran x = ⋃ ran ⋃ ran a$
37		suceq	$⊢ ⋃ ran ⋃ ran x = ⋃ ran ⋃ ran a \to suc ⋃ ran ⋃ ran x = suc ⋃ ran ⋃ ran a$
38	36 37	syl	$⊢ x = a \to suc ⋃ ran ⋃ ran x = suc ⋃ ran ⋃ ran a$
39	38	oveq1d	$⊢ x = a \to suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (b) = suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)$
40		fveq1	$⊢ x = a \to x (suc rank (b)) = a (suc rank (b))$
41	40	fveq1d	$⊢ x = a \to x (suc rank (b)) (b) = a (suc rank (b)) (b)$
42	39 41	oveq12d	$⊢ x = a \to (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (b)) +_{𝑜} x (suc rank (b)) (b) = (suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)) +_{𝑜} a (suc rank (b)) (b)$
43		id	$⊢ x = a \to x = a$
44	43 31	fveq12d	$⊢ x = a \to x (⋃ dom x) = a (⋃ dom a)$
45	44	rneqd	$⊢ x = a \to ran x (⋃ dom x) = ran a (⋃ dom a)$
46		oieq2	$⊢ ran x (⋃ dom x) = ran a (⋃ dom a) \to OrdIso (E, ran x (⋃ dom x)) = OrdIso (E, ran a (⋃ dom a))$
47	45 46	syl	$⊢ x = a \to OrdIso (E, ran x (⋃ dom x)) = OrdIso (E, ran a (⋃ dom a))$
48	47	cnveqd	$⊢ x = a \to {OrdIso (E, ran x (⋃ dom x))}^{-1} = {OrdIso (E, ran a (⋃ dom a))}^{-1}$
49	48 44	coeq12d	$⊢ x = a \to {OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x) = {OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)$
50	49	imaeq1d	$⊢ x = a \to ({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [b] = ({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b]$
51	50	fveq2d	$⊢ x = a \to f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [b]) = f (({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b])$
52	32 42 51	ifbieq12d	$⊢ x = a \to if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (b)) +_{𝑜} x (suc rank (b)) (b), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [b])) = if (dom a = ⋃ dom a, (suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)) +_{𝑜} a (suc rank (b)) (b), f (({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b]))$
53	30 52	mpteq12dv	$⊢ x = a \to (b \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (b)) +_{𝑜} x (suc rank (b)) (b), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [b]))) = (b \in R_{1} (dom a) ⟼ if (dom a = ⋃ dom a, (suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)) +_{𝑜} a (suc rank (b)) (b), f (({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b])))$
54	28 53	syl5eq	$⊢ x = a \to (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y]))) = (b \in R_{1} (dom a) ⟼ if (dom a = ⋃ dom a, (suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)) +_{𝑜} a (suc rank (b)) (b), f (({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b])))$
55	54	cbvmptv	$⊢ (x \in V ⟼ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y])))) = (a \in V ⟼ (b \in R_{1} (dom a) ⟼ if (dom a = ⋃ dom a, (suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)) +_{𝑜} a (suc rank (b)) (b), f (({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b]))))$
56		recseq	$⊢ (x \in V ⟼ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y])))) = (a \in V ⟼ (b \in R_{1} (dom a) ⟼ if (dom a = ⋃ dom a, (suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)) +_{𝑜} a (suc rank (b)) (b), f (({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b])))) \to recs ((x \in V ⟼ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y]))))) = recs ((a \in V ⟼ (b \in R_{1} (dom a) ⟼ if (dom a = ⋃ dom a, (suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)) +_{𝑜} a (suc rank (b)) (b), f (({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b])))))$
57	55 56	ax-mp	$⊢ recs ((x \in V ⟼ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), f (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y]))))) = recs ((a \in V ⟼ (b \in R_{1} (dom a) ⟼ if (dom a = ⋃ dom a, (suc ⋃ ran ⋃ ran a \cdot_{𝑜} rank (b)) +_{𝑜} a (suc rank (b)) (b), f (({OrdIso (E, ran a (⋃ dom a))}^{-1} \circ a (⋃ dom a)) [b])))))$
58	10 16 57	dfac12lem3	$⊢ (f : 𝒫 har (R_{1} (z)) \underset{1-1 onto}{⟶} card (𝒫 har (R_{1} (z))) \land z \in On) \to R_{1} (z) \in dom card$
59	58	ex	$⊢ f : 𝒫 har (R_{1} (z)) \underset{1-1 onto}{⟶} card (𝒫 har (R_{1} (z))) \to (z \in On \to R_{1} (z) \in dom card)$
60	59	exlimiv	$⊢ \exists f f : 𝒫 har (R_{1} (z)) \underset{1-1 onto}{⟶} card (𝒫 har (R_{1} (z))) \to (z \in On \to R_{1} (z) \in dom card)$
61	9 60	sylbi	$⊢ 𝒫 har (R_{1} (z)) \approx card (𝒫 har (R_{1} (z))) \to (z \in On \to R_{1} (z) \in dom card)$
62	6 7 8 61	4syl	$⊢ \forall x \in On 𝒫 x \in dom card \to (z \in On \to R_{1} (z) \in dom card)$
63	62	imp	$⊢ (\forall x \in On 𝒫 x \in dom card \land z \in On) \to R_{1} (z) \in dom card$
64		r1suc	$⊢ z \in On \to R_{1} (suc z) = 𝒫 R_{1} (z)$
65	64	adantl	$⊢ (\forall x \in On 𝒫 x \in dom card \land z \in On) \to R_{1} (suc z) = 𝒫 R_{1} (z)$
66	65	eleq2d	$⊢ (\forall x \in On 𝒫 x \in dom card \land z \in On) \to (y \in R_{1} (suc z) \leftrightarrow y \in 𝒫 R_{1} (z))$
67		elpwi	$⊢ y \in 𝒫 R_{1} (z) \to y \subseteq R_{1} (z)$
68	66 67	syl6bi	$⊢ (\forall x \in On 𝒫 x \in dom card \land z \in On) \to (y \in R_{1} (suc z) \to y \subseteq R_{1} (z))$
69		ssnum	$⊢ (R_{1} (z) \in dom card \land y \subseteq R_{1} (z)) \to y \in dom card$
70	63 68 69	syl6an	$⊢ (\forall x \in On 𝒫 x \in dom card \land z \in On) \to (y \in R_{1} (suc z) \to y \in dom card)$
71	70	rexlimdva	$⊢ \forall x \in On 𝒫 x \in dom card \to (\exists z \in On y \in R_{1} (suc z) \to y \in dom card)$
72	1 71	syl5bi	$⊢ \forall x \in On 𝒫 x \in dom card \to (y \in ⋃ R_{1} [On] \to y \in dom card)$
73	72	ssrdv	$⊢ \forall x \in On 𝒫 x \in dom card \to ⋃ R_{1} [On] \subseteq dom card$
74		onwf	$⊢ On \subseteq ⋃ R_{1} [On]$
75	74	sseli	$⊢ x \in On \to x \in ⋃ R_{1} [On]$
76		pwwf	$⊢ x \in ⋃ R_{1} [On] \leftrightarrow 𝒫 x \in ⋃ R_{1} [On]$
77	75 76	sylib	$⊢ x \in On \to 𝒫 x \in ⋃ R_{1} [On]$
78		ssel	$⊢ ⋃ R_{1} [On] \subseteq dom card \to (𝒫 x \in ⋃ R_{1} [On] \to 𝒫 x \in dom card)$
79	77 78	syl5	$⊢ ⋃ R_{1} [On] \subseteq dom card \to (x \in On \to 𝒫 x \in dom card)$
80	79	ralrimiv	$⊢ ⋃ R_{1} [On] \subseteq dom card \to \forall x \in On 𝒫 x \in dom card$
81	73 80	impbii	$⊢ \forall x \in On 𝒫 x \in dom card \leftrightarrow ⋃ R_{1} [On] \subseteq dom card$

Metamath Proof Explorer

Theorem dfac12r

Proof