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	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 <_Q 𝑦 ∧ ¬ ( *_Q ‘ 𝑦 ) ∈ 𝐴 ) }
	Assertion	reclem2pr	⊢ ( 𝐴 ∈ P → 𝐵 ∈ P )

Proof

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

Metamath Proof Explorer

Theorem reclem2pr

Proof