Metamath Proof Explorer

Theorem 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 )