Step | Hyp | Ref
| Expression |
1 | | ltrelpr 10511 |
. . . . . . . . 9
⊢
<P ⊆ (P ×
P) |
2 | 1 | brel 5598 |
. . . . . . . 8
⊢ (𝑦<P
𝑥 → (𝑦 ∈ P ∧
𝑥 ∈
P)) |
3 | 2 | simpld 498 |
. . . . . . 7
⊢ (𝑦<P
𝑥 → 𝑦 ∈ P) |
4 | 3 | ralimi 3076 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 𝑦<P 𝑥 → ∀𝑦 ∈ 𝐴 𝑦 ∈ P) |
5 | | dfss3 3875 |
. . . . . 6
⊢ (𝐴 ⊆ P ↔
∀𝑦 ∈ 𝐴 𝑦 ∈ P) |
6 | 4, 5 | sylibr 237 |
. . . . 5
⊢
(∀𝑦 ∈
𝐴 𝑦<P 𝑥 → 𝐴 ⊆ P) |
7 | 6 | rexlimivw 3193 |
. . . 4
⊢
(∃𝑥 ∈
P ∀𝑦
∈ 𝐴 𝑦<P 𝑥 → 𝐴 ⊆ P) |
8 | 7 | adantl 485 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P
∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → 𝐴 ⊆ P) |
9 | | n0 4245 |
. . . . 5
⊢ (𝐴 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐴) |
10 | | ssel 3880 |
. . . . . . 7
⊢ (𝐴 ⊆ P →
(𝑧 ∈ 𝐴 → 𝑧 ∈ P)) |
11 | | prn0 10502 |
. . . . . . . . . 10
⊢ (𝑧 ∈ P →
𝑧 ≠
∅) |
12 | | 0pss 4344 |
. . . . . . . . . 10
⊢ (∅
⊊ 𝑧 ↔ 𝑧 ≠ ∅) |
13 | 11, 12 | sylibr 237 |
. . . . . . . . 9
⊢ (𝑧 ∈ P →
∅ ⊊ 𝑧) |
14 | | elssuni 4838 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 → 𝑧 ⊆ ∪ 𝐴) |
15 | | psssstr 4007 |
. . . . . . . . 9
⊢ ((∅
⊊ 𝑧 ∧ 𝑧 ⊆ ∪ 𝐴)
→ ∅ ⊊ ∪ 𝐴) |
16 | 13, 14, 15 | syl2an 599 |
. . . . . . . 8
⊢ ((𝑧 ∈ P ∧
𝑧 ∈ 𝐴) → ∅ ⊊ ∪ 𝐴) |
17 | 16 | expcom 417 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → (𝑧 ∈ P → ∅
⊊ ∪ 𝐴)) |
18 | 10, 17 | sylcom 30 |
. . . . . 6
⊢ (𝐴 ⊆ P →
(𝑧 ∈ 𝐴 → ∅ ⊊ ∪ 𝐴)) |
19 | 18 | exlimdv 1940 |
. . . . 5
⊢ (𝐴 ⊆ P →
(∃𝑧 𝑧 ∈ 𝐴 → ∅ ⊊ ∪ 𝐴)) |
20 | 9, 19 | syl5bi 245 |
. . . 4
⊢ (𝐴 ⊆ P →
(𝐴 ≠ ∅ →
∅ ⊊ ∪ 𝐴)) |
21 | | prpssnq 10503 |
. . . . . . 7
⊢ (𝑥 ∈ P →
𝑥 ⊊
Q) |
22 | 21 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ⊆ P ∧
𝑥 ∈ P)
→ 𝑥 ⊊
Q) |
23 | | ltprord 10543 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ P ∧
𝑥 ∈ P)
→ (𝑦<P 𝑥 ↔ 𝑦 ⊊ 𝑥)) |
24 | | pssss 3996 |
. . . . . . . . . 10
⊢ (𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥) |
25 | 23, 24 | syl6bi 256 |
. . . . . . . . 9
⊢ ((𝑦 ∈ P ∧
𝑥 ∈ P)
→ (𝑦<P 𝑥 → 𝑦 ⊆ 𝑥)) |
26 | 2, 25 | mpcom 38 |
. . . . . . . 8
⊢ (𝑦<P
𝑥 → 𝑦 ⊆ 𝑥) |
27 | 26 | ralimi 3076 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐴 𝑦<P 𝑥 → ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥) |
28 | | unissb 4840 |
. . . . . . 7
⊢ (∪ 𝐴
⊆ 𝑥 ↔
∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥) |
29 | 27, 28 | sylibr 237 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 𝑦<P 𝑥 → ∪ 𝐴
⊆ 𝑥) |
30 | | sspsstr 4006 |
. . . . . . 7
⊢ ((∪ 𝐴
⊆ 𝑥 ∧ 𝑥 ⊊ Q)
→ ∪ 𝐴 ⊊ Q) |
31 | 30 | expcom 417 |
. . . . . 6
⊢ (𝑥 ⊊ Q →
(∪ 𝐴 ⊆ 𝑥 → ∪ 𝐴 ⊊
Q)) |
32 | 22, 29, 31 | syl2im 40 |
. . . . 5
⊢ ((𝐴 ⊆ P ∧
𝑥 ∈ P)
→ (∀𝑦 ∈
𝐴 𝑦<P 𝑥 → ∪ 𝐴
⊊ Q)) |
33 | 32 | rexlimdva 3195 |
. . . 4
⊢ (𝐴 ⊆ P →
(∃𝑥 ∈
P ∀𝑦
∈ 𝐴 𝑦<P 𝑥 → ∪ 𝐴
⊊ Q)) |
34 | 20, 33 | anim12d 612 |
. . 3
⊢ (𝐴 ⊆ P →
((𝐴 ≠ ∅ ∧
∃𝑥 ∈
P ∀𝑦
∈ 𝐴 𝑦<P 𝑥) → (∅ ⊊ ∪ 𝐴
∧ ∪ 𝐴 ⊊
Q))) |
35 | 8, 34 | mpcom 38 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P
∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → (∅ ⊊ ∪ 𝐴
∧ ∪ 𝐴 ⊊ Q)) |
36 | | prcdnq 10506 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ P ∧
𝑥 ∈ 𝑧) → (𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧)) |
37 | 36 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ P →
(𝑥 ∈ 𝑧 → (𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧))) |
38 | 37 | com3r 87 |
. . . . . . . . . . 11
⊢ (𝑦 <Q
𝑥 → (𝑧 ∈ P →
(𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))) |
39 | 10, 38 | sylan9 511 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ P ∧
𝑦
<Q 𝑥) → (𝑧 ∈ 𝐴 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))) |
40 | 39 | reximdvai 3183 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ P ∧
𝑦
<Q 𝑥) → (∃𝑧 ∈ 𝐴 𝑥 ∈ 𝑧 → ∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧)) |
41 | | eluni2 4810 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝐴
↔ ∃𝑧 ∈
𝐴 𝑥 ∈ 𝑧) |
42 | | eluni2 4810 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑧 ∈
𝐴 𝑦 ∈ 𝑧) |
43 | 40, 41, 42 | 3imtr4g 299 |
. . . . . . . 8
⊢ ((𝐴 ⊆ P ∧
𝑦
<Q 𝑥) → (𝑥 ∈ ∪ 𝐴 → 𝑦 ∈ ∪ 𝐴)) |
44 | 43 | ex 416 |
. . . . . . 7
⊢ (𝐴 ⊆ P →
(𝑦
<Q 𝑥 → (𝑥 ∈ ∪ 𝐴 → 𝑦 ∈ ∪ 𝐴))) |
45 | 44 | com23 86 |
. . . . . 6
⊢ (𝐴 ⊆ P →
(𝑥 ∈ ∪ 𝐴
→ (𝑦
<Q 𝑥 → 𝑦 ∈ ∪ 𝐴))) |
46 | 45 | alrimdv 1936 |
. . . . 5
⊢ (𝐴 ⊆ P →
(𝑥 ∈ ∪ 𝐴
→ ∀𝑦(𝑦 <Q
𝑥 → 𝑦 ∈ ∪ 𝐴))) |
47 | | eluni 4809 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝐴
↔ ∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴)) |
48 | | prnmax 10508 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ P ∧
𝑥 ∈ 𝑧) → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦) |
49 | 48 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ P →
(𝑥 ∈ 𝑧 → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦)) |
50 | 10, 49 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ P →
(𝑧 ∈ 𝐴 → (𝑥 ∈ 𝑧 → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦))) |
51 | 50 | com23 86 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ P →
(𝑥 ∈ 𝑧 → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦))) |
52 | 51 | imp 410 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ P ∧
𝑥 ∈ 𝑧) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦)) |
53 | | ssrexv 3954 |
. . . . . . . . . 10
⊢ (𝑧 ⊆ ∪ 𝐴
→ (∃𝑦 ∈
𝑧 𝑥 <Q 𝑦 → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)) |
54 | 14, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 → (∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦 → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)) |
55 | 52, 54 | sylcom 30 |
. . . . . . . 8
⊢ ((𝐴 ⊆ P ∧
𝑥 ∈ 𝑧) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)) |
56 | 55 | expimpd 457 |
. . . . . . 7
⊢ (𝐴 ⊆ P →
((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)) |
57 | 56 | exlimdv 1940 |
. . . . . 6
⊢ (𝐴 ⊆ P →
(∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)) |
58 | 47, 57 | syl5bi 245 |
. . . . 5
⊢ (𝐴 ⊆ P →
(𝑥 ∈ ∪ 𝐴
→ ∃𝑦 ∈
∪ 𝐴𝑥 <Q 𝑦)) |
59 | 46, 58 | jcad 516 |
. . . 4
⊢ (𝐴 ⊆ P →
(𝑥 ∈ ∪ 𝐴
→ (∀𝑦(𝑦 <Q
𝑥 → 𝑦 ∈ ∪ 𝐴) ∧ ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))) |
60 | 59 | ralrimiv 3096 |
. . 3
⊢ (𝐴 ⊆ P →
∀𝑥 ∈ ∪ 𝐴(∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴) ∧ ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)) |
61 | 8, 60 | syl 17 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P
∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∀𝑥 ∈ ∪ 𝐴(∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴) ∧ ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)) |
62 | | elnp 10500 |
. 2
⊢ (∪ 𝐴
∈ P ↔ ((∅ ⊊ ∪
𝐴 ∧ ∪ 𝐴
⊊ Q) ∧ ∀𝑥 ∈ ∪ 𝐴(∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴) ∧ ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))) |
63 | 35, 61, 62 | sylanbrc 586 |
1
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P
∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∪ 𝐴
∈ P) |