acwer1prclem

		Ref	Expression
	Hypothesis	acwer1prclem.1	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
	Assertion	acwer1prclem	$⊢ (CHOICE \land ω ≼ A \land card (R_{1} (B)) = A) \to \exists s (card (s) \in card [W] \land card (s) = A)$

Proof

Step	Hyp	Ref	Expression
1		acwer1prclem.1	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
2		simp1	$⊢ (CHOICE \land ω ≼ A \land card (R_{1} (B)) = A) \to CHOICE$
3		breq2	$⊢ card (R_{1} (B)) = A \to (ω ≼ card (R_{1} (B)) \leftrightarrow ω ≼ A)$
4	3	biimpar	$⊢ (card (R_{1} (B)) = A \land ω ≼ A) \to ω ≼ card (R_{1} (B))$
5		fvex	$⊢ R_{1} (B) \in V$
6		acnum	$⊢ CHOICE \to (R_{1} (B) \in V \to R_{1} (B) \in dom card)$
7	5 6	mpi	$⊢ CHOICE \to R_{1} (B) \in dom card$
8		cardid2	$⊢ R_{1} (B) \in dom card \to card (R_{1} (B)) \approx R_{1} (B)$
9		domentr	$⊢ (ω ≼ card (R_{1} (B)) \land card (R_{1} (B)) \approx R_{1} (B)) \to ω ≼ R_{1} (B)$
10	8 9	sylan2	$⊢ (ω ≼ card (R_{1} (B)) \land R_{1} (B) \in dom card) \to ω ≼ R_{1} (B)$
11	7 10	sylan2	$⊢ (ω ≼ card (R_{1} (B)) \land CHOICE) \to ω ≼ R_{1} (B)$
12	11	expcom	$⊢ CHOICE \to (ω ≼ card (R_{1} (B)) \to ω ≼ R_{1} (B))$
13	4 12	syl5	$⊢ CHOICE \to ((card (R_{1} (B)) = A \land ω ≼ A) \to ω ≼ R_{1} (B))$
14	13	ancomsd	$⊢ CHOICE \to ((ω ≼ A \land card (R_{1} (B)) = A) \to ω ≼ R_{1} (B))$
15	14	3impib	$⊢ (CHOICE \land ω ≼ A \land card (R_{1} (B)) = A) \to ω ≼ R_{1} (B)$
16		dfac8	$⊢ CHOICE \leftrightarrow \forall z \exists y y We z$
17		weeq2	$⊢ z = R_{1} (B) \to (y We z \leftrightarrow y We R_{1} (B))$
18	17	exbidv	$⊢ z = R_{1} (B) \to (\exists y y We z \leftrightarrow \exists y y We R_{1} (B))$
19	5 18	spcv	$⊢ \forall z \exists y y We z \to \exists y y We R_{1} (B)$
20	16 19	sylbi	$⊢ CHOICE \to \exists y y We R_{1} (B)$
21		weexenwe	$⊢ (\exists y y We R_{1} (B) \land ω ≼ R_{1} (B)) \to \exists s (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land s \approx R_{1} (B))$
22	20 21	sylan	$⊢ (CHOICE \land ω ≼ R_{1} (B)) \to \exists s (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land s \approx R_{1} (B))$
23		carden2b	$⊢ s \approx R_{1} (B) \to card (s) = card (R_{1} (B))$
24	23	3anim3i	$⊢ (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land s \approx R_{1} (B)) \to (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land card (s) = card (R_{1} (B)))$
25	24	eximi	$⊢ \exists s (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land s \approx R_{1} (B)) \to \exists s (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land card (s) = card (R_{1} (B)))$
26	22 25	syl	$⊢ (CHOICE \land ω ≼ R_{1} (B)) \to \exists s (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land card (s) = card (R_{1} (B)))$
27	2 15 26	syl2anc	$⊢ (CHOICE \land ω ≼ A \land card (R_{1} (B)) = A) \to \exists s (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land card (s) = card (R_{1} (B)))$
28		df-3an	$⊢ (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land card (s) = card (R_{1} (B))) \leftrightarrow ((s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B)) \land card (s) = card (R_{1} (B)))$
29		fveq2	$⊢ x = B \to R_{1} (x) = R_{1} (B)$
30	29	sqxpeqd	$⊢ x = B \to R_{1} (x) \times R_{1} (x) = R_{1} (B) \times R_{1} (B)$
31	30	sseq2d	$⊢ x = B \to (s \subseteq R_{1} (x) \times R_{1} (x) \leftrightarrow s \subseteq R_{1} (B) \times R_{1} (B))$
32		eqidd	$⊢ x = B \to s = s$
33	32 29	weeq12d	$⊢ x = B \to (s We R_{1} (x) \leftrightarrow s We R_{1} (B))$
34	31 33	anbi12d	$⊢ x = B \to ((s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x)) \leftrightarrow (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B)))$
35	34	rspcev	$⊢ (B \in On \land (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B))) \to \exists x \in On (s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x))$
36		0elon	$⊢ \emptyset \in On$
37		r1fnon	$⊢ R_{1} Fn On$
38	37	fndmi	$⊢ dom R_{1} = On$
39	38	eleq2i	$⊢ B \in dom R_{1} \leftrightarrow B \in On$
40		ndmfv	$⊢ \neg B \in dom R_{1} \to R_{1} (B) = \emptyset$
41	39 40	sylnbir	$⊢ \neg B \in On \to R_{1} (B) = \emptyset$
42		r10	$⊢ R_{1} (\emptyset) = \emptyset$
43	41 42	eqtr4di	$⊢ \neg B \in On \to R_{1} (B) = R_{1} (\emptyset)$
44	43	sqxpeqd	$⊢ \neg B \in On \to R_{1} (B) \times R_{1} (B) = R_{1} (\emptyset) \times R_{1} (\emptyset)$
45	44	sseq2d	$⊢ \neg B \in On \to (s \subseteq R_{1} (B) \times R_{1} (B) \leftrightarrow s \subseteq R_{1} (\emptyset) \times R_{1} (\emptyset))$
46		eqidd	$⊢ \neg B \in On \to s = s$
47	46 43	weeq12d	$⊢ \neg B \in On \to (s We R_{1} (B) \leftrightarrow s We R_{1} (\emptyset))$
48	45 47	anbi12d	$⊢ \neg B \in On \to ((s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B)) \leftrightarrow (s \subseteq R_{1} (\emptyset) \times R_{1} (\emptyset) \land s We R_{1} (\emptyset)))$
49	48	biimpa	$⊢ (\neg B \in On \land (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B))) \to (s \subseteq R_{1} (\emptyset) \times R_{1} (\emptyset) \land s We R_{1} (\emptyset))$
50		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
51	50	sqxpeqd	$⊢ x = \emptyset \to R_{1} (x) \times R_{1} (x) = R_{1} (\emptyset) \times R_{1} (\emptyset)$
52	51	sseq2d	$⊢ x = \emptyset \to (s \subseteq R_{1} (x) \times R_{1} (x) \leftrightarrow s \subseteq R_{1} (\emptyset) \times R_{1} (\emptyset))$
53		eqidd	$⊢ x = \emptyset \to s = s$
54	53 50	weeq12d	$⊢ x = \emptyset \to (s We R_{1} (x) \leftrightarrow s We R_{1} (\emptyset))$
55	52 54	anbi12d	$⊢ x = \emptyset \to ((s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x)) \leftrightarrow (s \subseteq R_{1} (\emptyset) \times R_{1} (\emptyset) \land s We R_{1} (\emptyset)))$
56	55	rspcev	$⊢ (\emptyset \in On \land (s \subseteq R_{1} (\emptyset) \times R_{1} (\emptyset) \land s We R_{1} (\emptyset))) \to \exists x \in On (s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x))$
57	36 49 56	sylancr	$⊢ (\neg B \in On \land (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B))) \to \exists x \in On (s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x))$
58	35 57	pm2.61ian	$⊢ (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B)) \to \exists x \in On (s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x))$
59		vex	$⊢ s \in V$
60		sseq1	$⊢ r = s \to (r \subseteq R_{1} (x) \times R_{1} (x) \leftrightarrow s \subseteq R_{1} (x) \times R_{1} (x))$
61		weeq1	$⊢ r = s \to (r We R_{1} (x) \leftrightarrow s We R_{1} (x))$
62	60 61	anbi12d	$⊢ r = s \to ((r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x)) \leftrightarrow (s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x)))$
63	62	rexbidv	$⊢ r = s \to (\exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x)) \leftrightarrow \exists x \in On (s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x)))$
64	59 63 1	elab2	$⊢ s \in W \leftrightarrow \exists x \in On (s \subseteq R_{1} (x) \times R_{1} (x) \land s We R_{1} (x))$
65	58 64	sylibr	$⊢ (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B)) \to s \in W$
66		acnum	$⊢ CHOICE \to (s \in W \to s \in dom card)$
67		cardf2	$⊢ card : \{v \| \exists w \in On w \approx v\} ⟶ On$
68		ffun	$⊢ card : \{v \| \exists w \in On w \approx v\} ⟶ On \to Fun card$
69	67 68	ax-mp	$⊢ Fun card$
70		funfvima	$⊢ (Fun card \land s \in dom card) \to (s \in W \to card (s) \in card [W])$
71	69 70	mpan	$⊢ s \in dom card \to (s \in W \to card (s) \in card [W])$
72	66 71	syli	$⊢ CHOICE \to (s \in W \to card (s) \in card [W])$
73		eqtr	$⊢ (card (s) = card (R_{1} (B)) \land card (R_{1} (B)) = A) \to card (s) = A$
74	73	expcom	$⊢ card (R_{1} (B)) = A \to (card (s) = card (R_{1} (B)) \to card (s) = A)$
75	72 74	im2anan9	$⊢ (CHOICE \land card (R_{1} (B)) = A) \to ((s \in W \land card (s) = card (R_{1} (B))) \to (card (s) \in card [W] \land card (s) = A))$
76	65 75	sylani	$⊢ (CHOICE \land card (R_{1} (B)) = A) \to (((s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B)) \land card (s) = card (R_{1} (B))) \to (card (s) \in card [W] \land card (s) = A))$
77	28 76	biimtrid	$⊢ (CHOICE \land card (R_{1} (B)) = A) \to ((s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land card (s) = card (R_{1} (B))) \to (card (s) \in card [W] \land card (s) = A))$
78	77	eximdv	$⊢ (CHOICE \land card (R_{1} (B)) = A) \to (\exists s (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land card (s) = card (R_{1} (B))) \to \exists s (card (s) \in card [W] \land card (s) = A))$
79	78	3adant2	$⊢ (CHOICE \land ω ≼ A \land card (R_{1} (B)) = A) \to (\exists s (s \subseteq R_{1} (B) \times R_{1} (B) \land s We R_{1} (B) \land card (s) = card (R_{1} (B))) \to \exists s (card (s) \in card [W] \land card (s) = A))$
80	27 79	mpd	$⊢ (CHOICE \land ω ≼ A \land card (R_{1} (B)) = A) \to \exists s (card (s) \in card [W] \land card (s) = A)$

Metamath Proof Explorer

Theorem acwer1prclem

Proof