Step | Hyp | Ref
| Expression |
1 | | elpwi 4117 |
. . . 4
⊢ (𝑦 ∈ 𝒫 𝒫
𝐴 → 𝑦 ⊆ 𝒫 𝐴) |
2 | | fin2i2 9023 |
. . . . 5
⊢ (((𝐴 ∈ FinII ∧
𝑦 ⊆ 𝒫 𝐴) ∧ (𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) → ∩ 𝑦
∈ 𝑦) |
3 | 2 | ex 449 |
. . . 4
⊢ ((𝐴 ∈ FinII ∧
𝑦 ⊆ 𝒫 𝐴) → ((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦)) |
4 | 1, 3 | sylan2 490 |
. . 3
⊢ ((𝐴 ∈ FinII ∧
𝑦 ∈ 𝒫
𝒫 𝐴) → ((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
→ ∩ 𝑦 ∈ 𝑦)) |
5 | 4 | ralrimiva 2949 |
. 2
⊢ (𝐴 ∈ FinII →
∀𝑦 ∈ 𝒫
𝒫 𝐴((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
→ ∩ 𝑦 ∈ 𝑦)) |
6 | | elpwi 4117 |
. . . . 5
⊢ (𝑏 ∈ 𝒫 𝒫
𝐴 → 𝑏 ⊆ 𝒫 𝐴) |
7 | | simp1r 1079 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ 𝑏 ⊆ 𝒫
𝐴) |
8 | | ssrab2 3650 |
. . . . . . . . . . 11
⊢ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴 |
9 | | simp1l 1078 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ 𝐴 ∈ 𝑉) |
10 | | pwexg 4776 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
11 | | elpw2g 4754 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∈
V → ({𝑐 ∈
𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴 ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴)) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ({𝑐 ∈ 𝒫
𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴 ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴)) |
13 | 8, 12 | mpbiri 247 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ {𝑐 ∈ 𝒫
𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴) |
14 | | simp2 1055 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∀𝑦 ∈
𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦)) |
15 | | simp3l 1082 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ 𝑏 ≠
∅) |
16 | | fin23lem7 9021 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ∧ 𝑏 ≠ ∅) → {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅) |
17 | 9, 7, 15, 16 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ {𝑐 ∈ 𝒫
𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅) |
18 | | sorpsscmpl 6846 |
. . . . . . . . . . . . 13
⊢ (
[⊊] Or 𝑏
→ [⊊] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
19 | 18 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ [⊊] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
20 | 19 | 3ad2ant3 1077 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ [⊊] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
21 | 17, 20 | jca 553 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ({𝑐 ∈ 𝒫
𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅ ∧ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
22 | | neeq1 2844 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → (𝑦 ≠ ∅ ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅)) |
23 | | soeq2 4979 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → ( [⊊] Or 𝑦 ↔ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
24 | 22, 23 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → ((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) ↔ ({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅ ∧ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}))) |
25 | | inteq 4413 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → ∩ 𝑦 = ∩
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
26 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → 𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
27 | 25, 26 | eleq12d 2682 |
. . . . . . . . . . . 12
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → (∩ 𝑦 ∈ 𝑦 ↔ ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
28 | 24, 27 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → (((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ↔ (({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅ ∧ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) → ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}))) |
29 | 28 | rspcv 3278 |
. . . . . . . . . 10
⊢ ({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴 → (∀𝑦 ∈ 𝒫 𝒫
𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) → (({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅ ∧ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) → ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}))) |
30 | 13, 14, 21, 29 | syl3c 64 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
31 | | sorpssint 6845 |
. . . . . . . . . 10
⊢ (
[⊊] Or {𝑐
∈ 𝒫 𝐴 ∣
(𝐴 ∖ 𝑐) ∈ 𝑏} → (∃𝑧 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ¬ 𝑤 ⊊ 𝑧 ↔ ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
32 | 20, 31 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ (∃𝑧 ∈
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ¬ 𝑤 ⊊ 𝑧 ↔ ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
33 | 30, 32 | mpbird 246 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∃𝑧 ∈
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ¬ 𝑤 ⊊ 𝑧) |
34 | | psseq1 3656 |
. . . . . . . . 9
⊢ (𝑚 = (𝐴 ∖ 𝑧) → (𝑚 ⊊ 𝑛 ↔ (𝐴 ∖ 𝑧) ⊊ 𝑛)) |
35 | | psseq1 3656 |
. . . . . . . . 9
⊢ (𝑤 = (𝐴 ∖ 𝑛) → (𝑤 ⊊ 𝑧 ↔ (𝐴 ∖ 𝑛) ⊊ 𝑧)) |
36 | | pssdifcom1 4006 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐴) → ((𝐴 ∖ 𝑧) ⊊ 𝑛 ↔ (𝐴 ∖ 𝑛) ⊊ 𝑧)) |
37 | 34, 35, 36 | fin23lem11 9022 |
. . . . . . . 8
⊢ (𝑏 ⊆ 𝒫 𝐴 → (∃𝑧 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ¬ 𝑤 ⊊ 𝑧 → ∃𝑚 ∈ 𝑏 ∀𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛)) |
38 | 7, 33, 37 | sylc 63 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∃𝑚 ∈
𝑏 ∀𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛) |
39 | | simp3r 1083 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ [⊊] Or 𝑏) |
40 | | sorpssuni 6844 |
. . . . . . . 8
⊢ (
[⊊] Or 𝑏
→ (∃𝑚 ∈
𝑏 ∀𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛 ↔ ∪ 𝑏 ∈ 𝑏)) |
41 | 39, 40 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ (∃𝑚 ∈
𝑏 ∀𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛 ↔ ∪ 𝑏 ∈ 𝑏)) |
42 | 38, 41 | mpbid 221 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∪ 𝑏 ∈ 𝑏) |
43 | 42 | 3exp 1256 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) → ((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ ∪ 𝑏 ∈ 𝑏))) |
44 | 6, 43 | sylan2 490 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝒫 𝒫 𝐴) → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) → ((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ ∪ 𝑏 ∈ 𝑏))) |
45 | 44 | ralrimdva 2952 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) →
∀𝑏 ∈ 𝒫
𝒫 𝐴((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ ∪ 𝑏 ∈ 𝑏))) |
46 | | isfin2 8999 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinII ↔
∀𝑏 ∈ 𝒫
𝒫 𝐴((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ ∪ 𝑏 ∈ 𝑏))) |
47 | 45, 46 | sylibrd 248 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) → 𝐴 ∈
FinII)) |
48 | 5, 47 | impbid2 215 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinII ↔
∀𝑦 ∈ 𝒫
𝒫 𝐴((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
→ ∩ 𝑦 ∈ 𝑦))) |