reclem2pr

Description: Lemma for Proposition 9-3.7 of Gleason p. 124. (Contributed by NM, 30-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	reclempr.1	$⊢ B = \{x \| \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A)\}$
	Assertion	reclem2pr	$⊢ A \in 𝑷 \to B \in 𝑷$

Proof

Step	Hyp	Ref	Expression
1		reclempr.1	$⊢ B = \{x \| \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A)\}$
2		prpssnq	$⊢ A \in 𝑷 \to A \subset 𝑸$
3		pssnel	$⊢ A \subset 𝑸 \to \exists x (x \in 𝑸 \land \neg x \in A)$
4		recclnq	$⊢ x \in 𝑸 \to *_{𝑸} (x) \in 𝑸$
5		nsmallnq	$⊢ _{𝑸} (x) \in 𝑸 \to \exists z z <_{𝑸} _{𝑸} (x)$
6	4 5	syl	$⊢ x \in 𝑸 \to \exists z z <_{𝑸} *_{𝑸} (x)$
7	6	adantr	$⊢ (x \in 𝑸 \land \neg x \in A) \to \exists z z <_{𝑸} *_{𝑸} (x)$
8		recrecnq	$⊢ x \in 𝑸 \to _{𝑸} (_{𝑸} (x)) = x$
9	8	eleq1d	$⊢ x \in 𝑸 \to (_{𝑸} (_{𝑸} (x)) \in A \leftrightarrow x \in A)$
10	9	notbid	$⊢ x \in 𝑸 \to (\neg _{𝑸} (_{𝑸} (x)) \in A \leftrightarrow \neg x \in A)$
11	10	anbi2d	$⊢ x \in 𝑸 \to ((z <_{𝑸} _{𝑸} (x) \land \neg _{𝑸} (_{𝑸} (x)) \in A) \leftrightarrow (z <_{𝑸} _{𝑸} (x) \land \neg x \in A))$
12		fvex	$⊢ *_{𝑸} (x) \in V$
13		breq2	$⊢ y = _{𝑸} (x) \to (z <_{𝑸} y \leftrightarrow z <_{𝑸} _{𝑸} (x))$
14		fveq2	$⊢ y = _{𝑸} (x) \to _{𝑸} (y) = _{𝑸} (_{𝑸} (x))$
15	14	eleq1d	$⊢ y = _{𝑸} (x) \to (_{𝑸} (y) \in A \leftrightarrow _{𝑸} (_{𝑸} (x)) \in A)$
16	15	notbid	$⊢ y = _{𝑸} (x) \to (\neg _{𝑸} (y) \in A \leftrightarrow \neg _{𝑸} (_{𝑸} (x)) \in A)$
17	13 16	anbi12d	$⊢ y = _{𝑸} (x) \to ((z <_{𝑸} y \land \neg _{𝑸} (y) \in A) \leftrightarrow (z <_{𝑸} _{𝑸} (x) \land \neg _{𝑸} (*_{𝑸} (x)) \in A))$
18	12 17	spcev	$⊢ (z <_{𝑸} _{𝑸} (x) \land \neg _{𝑸} (_{𝑸} (x)) \in A) \to \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)$
19	11 18	biimtrrdi	$⊢ x \in 𝑸 \to ((z <_{𝑸} _{𝑸} (x) \land \neg x \in A) \to \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A))$
20		vex	$⊢ z \in V$
21		breq1	$⊢ x = z \to (x <_{𝑸} y \leftrightarrow z <_{𝑸} y)$
22	21	anbi1d	$⊢ x = z \to ((x <_{𝑸} y \land \neg _{𝑸} (y) \in A) \leftrightarrow (z <_{𝑸} y \land \neg _{𝑸} (y) \in A))$
23	22	exbidv	$⊢ x = z \to (\exists y (x <_{𝑸} y \land \neg _{𝑸} (y) \in A) \leftrightarrow \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A))$
24	20 23 1	elab2	$⊢ z \in B \leftrightarrow \exists y (z <_{𝑸} y \land \neg *_{𝑸} (y) \in A)$
25	19 24	imbitrrdi	$⊢ x \in 𝑸 \to ((z <_{𝑸} *_{𝑸} (x) \land \neg x \in A) \to z \in B)$
26	25	expcomd	$⊢ x \in 𝑸 \to (\neg x \in A \to (z <_{𝑸} *_{𝑸} (x) \to z \in B))$
27	26	imp	$⊢ (x \in 𝑸 \land \neg x \in A) \to (z <_{𝑸} *_{𝑸} (x) \to z \in B)$
28	27	eximdv	$⊢ (x \in 𝑸 \land \neg x \in A) \to (\exists z z <_{𝑸} *_{𝑸} (x) \to \exists z z \in B)$
29	7 28	mpd	$⊢ (x \in 𝑸 \land \neg x \in A) \to \exists z z \in B$
30		n0	$⊢ B \neq \emptyset \leftrightarrow \exists z z \in B$
31	29 30	sylibr	$⊢ (x \in 𝑸 \land \neg x \in A) \to B \neq \emptyset$
32	31	exlimiv	$⊢ \exists x (x \in 𝑸 \land \neg x \in A) \to B \neq \emptyset$
33	2 3 32	3syl	$⊢ A \in 𝑷 \to B \neq \emptyset$
34		0pss	$⊢ \emptyset \subset B \leftrightarrow B \neq \emptyset$
35	33 34	sylibr	$⊢ A \in 𝑷 \to \emptyset \subset B$
36		prn0	$⊢ A \in 𝑷 \to A \neq \emptyset$
37		elprnq	$⊢ (A \in 𝑷 \land z \in A) \to z \in 𝑸$
38		recrecnq	$⊢ z \in 𝑸 \to _{𝑸} (_{𝑸} (z)) = z$
39	38	eleq1d	$⊢ z \in 𝑸 \to (_{𝑸} (_{𝑸} (z)) \in A \leftrightarrow z \in A)$
40	39	anbi2d	$⊢ z \in 𝑸 \to ((A \in 𝑷 \land _{𝑸} (_{𝑸} (z)) \in A) \leftrightarrow (A \in 𝑷 \land z \in A))$
41	37 40	syl	$⊢ (A \in 𝑷 \land z \in A) \to ((A \in 𝑷 \land _{𝑸} (_{𝑸} (z)) \in A) \leftrightarrow (A \in 𝑷 \land z \in A))$
42		fvex	$⊢ *_{𝑸} (z) \in V$
43		fveq2	$⊢ x = _{𝑸} (z) \to _{𝑸} (x) = _{𝑸} (_{𝑸} (z))$
44	43	eleq1d	$⊢ x = _{𝑸} (z) \to (_{𝑸} (x) \in A \leftrightarrow _{𝑸} (_{𝑸} (z)) \in A)$
45	44	anbi2d	$⊢ x = _{𝑸} (z) \to ((A \in 𝑷 \land _{𝑸} (x) \in A) \leftrightarrow (A \in 𝑷 \land _{𝑸} (_{𝑸} (z)) \in A))$
46	42 45	spcev	$⊢ (A \in 𝑷 \land _{𝑸} (_{𝑸} (z)) \in A) \to \exists x (A \in 𝑷 \land *_{𝑸} (x) \in A)$
47	41 46	biimtrrdi	$⊢ (A \in 𝑷 \land z \in A) \to ((A \in 𝑷 \land z \in A) \to \exists x (A \in 𝑷 \land *_{𝑸} (x) \in A))$
48	47	pm2.43i	$⊢ (A \in 𝑷 \land z \in A) \to \exists x (A \in 𝑷 \land *_{𝑸} (x) \in A)$
49		elprnq	$⊢ (A \in 𝑷 \land _{𝑸} (x) \in A) \to _{𝑸} (x) \in 𝑸$
50		dmrecnq	$⊢ dom *_{𝑸} = 𝑸$
51		0nnq	$⊢ \neg \emptyset \in 𝑸$
52	50 51	ndmfvrcl	$⊢ *_{𝑸} (x) \in 𝑸 \to x \in 𝑸$
53	49 52	syl	$⊢ (A \in 𝑷 \land *_{𝑸} (x) \in A) \to x \in 𝑸$
54		ltrnq	$⊢ x <_{𝑸} y \leftrightarrow _{𝑸} (y) <_{𝑸} _{𝑸} (x)$
55		prcdnq	$⊢ (A \in 𝑷 \land _{𝑸} (x) \in A) \to (_{𝑸} (y) <_{𝑸} _{𝑸} (x) \to _{𝑸} (y) \in A)$
56	54 55	biimtrid	$⊢ (A \in 𝑷 \land _{𝑸} (x) \in A) \to (x <_{𝑸} y \to _{𝑸} (y) \in A)$
57	56	alrimiv	$⊢ (A \in 𝑷 \land _{𝑸} (x) \in A) \to \forall y (x <_{𝑸} y \to _{𝑸} (y) \in A)$
58	1	eqabri	$⊢ x \in B \leftrightarrow \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A)$
59		exanali	$⊢ \exists y (x <_{𝑸} y \land \neg _{𝑸} (y) \in A) \leftrightarrow \neg \forall y (x <_{𝑸} y \to _{𝑸} (y) \in A)$
60	58 59	bitri	$⊢ x \in B \leftrightarrow \neg \forall y (x <_{𝑸} y \to *_{𝑸} (y) \in A)$
61	60	con2bii	$⊢ \forall y (x <_{𝑸} y \to *_{𝑸} (y) \in A) \leftrightarrow \neg x \in B$
62	57 61	sylib	$⊢ (A \in 𝑷 \land *_{𝑸} (x) \in A) \to \neg x \in B$
63	53 62	jca	$⊢ (A \in 𝑷 \land *_{𝑸} (x) \in A) \to (x \in 𝑸 \land \neg x \in B)$
64	63	eximi	$⊢ \exists x (A \in 𝑷 \land *_{𝑸} (x) \in A) \to \exists x (x \in 𝑸 \land \neg x \in B)$
65	48 64	syl	$⊢ (A \in 𝑷 \land z \in A) \to \exists x (x \in 𝑸 \land \neg x \in B)$
66	65	ex	$⊢ A \in 𝑷 \to (z \in A \to \exists x (x \in 𝑸 \land \neg x \in B))$
67	66	exlimdv	$⊢ A \in 𝑷 \to (\exists z z \in A \to \exists x (x \in 𝑸 \land \neg x \in B))$
68		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
69		nss	$⊢ \neg 𝑸 \subseteq B \leftrightarrow \exists x (x \in 𝑸 \land \neg x \in B)$
70	67 68 69	3imtr4g	$⊢ A \in 𝑷 \to (A \neq \emptyset \to \neg 𝑸 \subseteq B)$
71	36 70	mpd	$⊢ A \in 𝑷 \to \neg 𝑸 \subseteq B$
72		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
73	72	brel	$⊢ x <_{𝑸} y \to (x \in 𝑸 \land y \in 𝑸)$
74	73	simpld	$⊢ x <_{𝑸} y \to x \in 𝑸$
75	74	adantr	$⊢ (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to x \in 𝑸$
76	75	exlimiv	$⊢ \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to x \in 𝑸$
77	58 76	sylbi	$⊢ x \in B \to x \in 𝑸$
78	77	ssriv	$⊢ B \subseteq 𝑸$
79	71 78	jctil	$⊢ A \in 𝑷 \to (B \subseteq 𝑸 \land \neg 𝑸 \subseteq B)$
80		dfpss3	$⊢ B \subset 𝑸 \leftrightarrow (B \subseteq 𝑸 \land \neg 𝑸 \subseteq B)$
81	79 80	sylibr	$⊢ A \in 𝑷 \to B \subset 𝑸$
82	35 81	jca	$⊢ A \in 𝑷 \to (\emptyset \subset B \land B \subset 𝑸)$
83		ltsonq	$⊢ <_{𝑸} Or 𝑸$
84	83 72	sotri	$⊢ (z <_{𝑸} x \land x <_{𝑸} y) \to z <_{𝑸} y$
85	84	ex	$⊢ z <_{𝑸} x \to (x <_{𝑸} y \to z <_{𝑸} y)$
86	85	anim1d	$⊢ z <_{𝑸} x \to ((x <_{𝑸} y \land \neg _{𝑸} (y) \in A) \to (z <_{𝑸} y \land \neg _{𝑸} (y) \in A))$
87	86	eximdv	$⊢ z <_{𝑸} x \to (\exists y (x <_{𝑸} y \land \neg _{𝑸} (y) \in A) \to \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A))$
88	87 58 24	3imtr4g	$⊢ z <_{𝑸} x \to (x \in B \to z \in B)$
89	88	com12	$⊢ x \in B \to (z <_{𝑸} x \to z \in B)$
90	89	alrimiv	$⊢ x \in B \to \forall z (z <_{𝑸} x \to z \in B)$
91		nfe1	$⊢ Ⅎ y \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A)$
92	91	nfab	$⊢ \underline{Ⅎ} y \{x \| \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A)\}$
93	1 92	nfcxfr	$⊢ \underline{Ⅎ} y B$
94		nfv	$⊢ Ⅎ y x <_{𝑸} z$
95	93 94	nfrexw	$⊢ Ⅎ y \exists z \in B x <_{𝑸} z$
96		19.8a	$⊢ (z <_{𝑸} y \land \neg _{𝑸} (y) \in A) \to \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)$
97	96 24	sylibr	$⊢ (z <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to z \in B$
98	97	adantll	$⊢ ((x <_{𝑸} z \land z <_{𝑸} y) \land \neg *_{𝑸} (y) \in A) \to z \in B$
99		simpll	$⊢ ((x <_{𝑸} z \land z <_{𝑸} y) \land \neg *_{𝑸} (y) \in A) \to x <_{𝑸} z$
100	98 99	jca	$⊢ ((x <_{𝑸} z \land z <_{𝑸} y) \land \neg *_{𝑸} (y) \in A) \to (z \in B \land x <_{𝑸} z)$
101	100	expcom	$⊢ \neg *_{𝑸} (y) \in A \to ((x <_{𝑸} z \land z <_{𝑸} y) \to (z \in B \land x <_{𝑸} z))$
102	101	eximdv	$⊢ \neg *_{𝑸} (y) \in A \to (\exists z (x <_{𝑸} z \land z <_{𝑸} y) \to \exists z (z \in B \land x <_{𝑸} z))$
103		ltbtwnnq	$⊢ x <_{𝑸} y \leftrightarrow \exists z (x <_{𝑸} z \land z <_{𝑸} y)$
104		df-rex	$⊢ \exists z \in B x <_{𝑸} z \leftrightarrow \exists z (z \in B \land x <_{𝑸} z)$
105	102 103 104	3imtr4g	$⊢ \neg *_{𝑸} (y) \in A \to (x <_{𝑸} y \to \exists z \in B x <_{𝑸} z)$
106	105	impcom	$⊢ (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to \exists z \in B x <_{𝑸} z$
107	95 106	exlimi	$⊢ \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to \exists z \in B x <_{𝑸} z$
108	58 107	sylbi	$⊢ x \in B \to \exists z \in B x <_{𝑸} z$
109	90 108	jca	$⊢ x \in B \to (\forall z (z <_{𝑸} x \to z \in B) \land \exists z \in B x <_{𝑸} z)$
110	109	rgen	$⊢ \forall x \in B (\forall z (z <_{𝑸} x \to z \in B) \land \exists z \in B x <_{𝑸} z)$
111		elnp	$⊢ B \in 𝑷 \leftrightarrow ((\emptyset \subset B \land B \subset 𝑸) \land \forall x \in B (\forall z (z <_{𝑸} x \to z \in B) \land \exists z \in B x <_{𝑸} z))$
112	82 110 111	sylanblrc	$⊢ A \in 𝑷 \to B \in 𝑷$

Metamath Proof Explorer

Theorem reclem2pr

Proof