Step | Hyp | Ref
| Expression |
1 | | recexpr.1 |
. . . 4
⊢ B = 〈{x
∣ ∃y(x
<Q y ∧ (*Q‘y) ∈
(2nd ‘A))}, {x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))}〉 |
2 | 1 | recexprlemm 6596 |
. . 3
⊢ (A ∈
P → (∃𝑞 ∈
Q 𝑞 ∈ (1st ‘B) ∧ ∃𝑟 ∈
Q 𝑟 ∈ (2nd ‘B))) |
3 | | ltrelnq 6349 |
. . . . . . . . . . 11
⊢
<Q ⊆ (Q ×
Q) |
4 | 3 | brel 4335 |
. . . . . . . . . 10
⊢ (x <Q y → (x
∈ Q ∧ y ∈ Q)) |
5 | 4 | simpld 105 |
. . . . . . . . 9
⊢ (x <Q y → x ∈ Q) |
6 | 5 | adantr 261 |
. . . . . . . 8
⊢
((x <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) → x
∈ Q) |
7 | 6 | exlimiv 1486 |
. . . . . . 7
⊢ (∃y(x <Q y ∧
(*Q‘y) ∈ (2nd ‘A)) → x
∈ Q) |
8 | 7 | abssi 3009 |
. . . . . 6
⊢ {x ∣ ∃y(x <Q y ∧
(*Q‘y) ∈ (2nd ‘A))} ⊆ Q |
9 | | nqex 6347 |
. . . . . . 7
⊢
Q ∈ V |
10 | 9 | elpw2 3902 |
. . . . . 6
⊢
({x ∣ ∃y(x <Q y ∧
(*Q‘y) ∈ (2nd ‘A))} ∈ 𝒫
Q ↔ {x ∣ ∃y(x <Q y ∧
(*Q‘y) ∈ (2nd ‘A))} ⊆ Q) |
11 | 8, 10 | mpbir 134 |
. . . . 5
⊢ {x ∣ ∃y(x <Q y ∧
(*Q‘y) ∈ (2nd ‘A))} ∈ 𝒫
Q |
12 | 3 | brel 4335 |
. . . . . . . . . 10
⊢ (y <Q x → (y
∈ Q ∧ x ∈ Q)) |
13 | 12 | simprd 107 |
. . . . . . . . 9
⊢ (y <Q x → x ∈ Q) |
14 | 13 | adantr 261 |
. . . . . . . 8
⊢
((y <Q
x ∧
(*Q‘y) ∈ (1st ‘A)) → x
∈ Q) |
15 | 14 | exlimiv 1486 |
. . . . . . 7
⊢ (∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A)) → x
∈ Q) |
16 | 15 | abssi 3009 |
. . . . . 6
⊢ {x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))} ⊆ Q |
17 | 9 | elpw2 3902 |
. . . . . 6
⊢
({x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))} ∈ 𝒫
Q ↔ {x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))} ⊆ Q) |
18 | 16, 17 | mpbir 134 |
. . . . 5
⊢ {x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))} ∈ 𝒫
Q |
19 | | opelxpi 4319 |
. . . . 5
⊢
(({x ∣ ∃y(x <Q y ∧
(*Q‘y) ∈ (2nd ‘A))} ∈ 𝒫
Q ∧ {x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))} ∈ 𝒫
Q) → 〈{x ∣
∃y(x
<Q y ∧ (*Q‘y) ∈
(2nd ‘A))}, {x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))}〉 ∈
(𝒫 Q × 𝒫 Q)) |
20 | 11, 18, 19 | mp2an 402 |
. . . 4
⊢
〈{x ∣ ∃y(x <Q y ∧
(*Q‘y) ∈ (2nd ‘A))}, {x ∣
∃y(y
<Q x ∧ (*Q‘y) ∈
(1st ‘A))}〉 ∈ (𝒫 Q × 𝒫
Q) |
21 | 1, 20 | eqeltri 2107 |
. . 3
⊢ B ∈ (𝒫
Q × 𝒫 Q) |
22 | 2, 21 | jctil 295 |
. 2
⊢ (A ∈
P → (B ∈ (𝒫 Q × 𝒫
Q) ∧ (∃𝑞 ∈
Q 𝑞 ∈ (1st ‘B) ∧ ∃𝑟 ∈
Q 𝑟 ∈ (2nd ‘B)))) |
23 | 1 | recexprlemrnd 6601 |
. . 3
⊢ (A ∈
P → (∀𝑞 ∈
Q (𝑞 ∈ (1st ‘B) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧
𝑟 ∈ (1st ‘B))) ∧ ∀𝑟 ∈
Q (𝑟 ∈ (2nd ‘B) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧
𝑞 ∈ (2nd ‘B))))) |
24 | 1 | recexprlemdisj 6602 |
. . 3
⊢ (A ∈
P → ∀𝑞 ∈
Q ¬ (𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B))) |
25 | 1 | recexprlemloc 6603 |
. . 3
⊢ (A ∈
P → ∀𝑞 ∈
Q ∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈
(1st ‘B) ∨ 𝑟
∈ (2nd ‘B)))) |
26 | 23, 24, 25 | 3jca 1083 |
. 2
⊢ (A ∈
P → ((∀𝑞 ∈
Q (𝑞 ∈ (1st ‘B) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧
𝑟 ∈ (1st ‘B))) ∧ ∀𝑟 ∈
Q (𝑟 ∈ (2nd ‘B) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧
𝑞 ∈ (2nd ‘B)))) ∧ ∀𝑞 ∈
Q ¬ (𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)) ∧ ∀𝑞 ∈
Q ∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈
(1st ‘B) ∨ 𝑟
∈ (2nd ‘B))))) |
27 | | elnp1st2nd 6459 |
. 2
⊢ (B ∈
P ↔ ((B ∈ (𝒫 Q × 𝒫
Q) ∧ (∃𝑞 ∈
Q 𝑞 ∈ (1st ‘B) ∧ ∃𝑟 ∈
Q 𝑟 ∈ (2nd ‘B))) ∧ ((∀𝑞 ∈
Q (𝑞 ∈ (1st ‘B) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧
𝑟 ∈ (1st ‘B))) ∧ ∀𝑟 ∈
Q (𝑟 ∈ (2nd ‘B) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧
𝑞 ∈ (2nd ‘B)))) ∧ ∀𝑞 ∈
Q ¬ (𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)) ∧ ∀𝑞 ∈
Q ∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈
(1st ‘B) ∨ 𝑟
∈ (2nd ‘B)))))) |
28 | 22, 26, 27 | sylanbrc 394 |
1
⊢ (A ∈
P → B ∈ P) |