Step | Hyp | Ref
| Expression |
1 | | elpwi 4168 |
. . . 4
⊢ (𝑦 ∈ 𝒫 𝒫
𝐴 → 𝑦 ⊆ 𝒫 𝐴) |
2 | | fin2i2 9140 |
. . . . 5
⊢ (((𝐴 ∈ FinII ∧
𝑦 ⊆ 𝒫 𝐴) ∧ (𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) → ∩ 𝑦
∈ 𝑦) |
3 | 2 | ex 450 |
. . . 4
⊢ ((𝐴 ∈ FinII ∧
𝑦 ⊆ 𝒫 𝐴) → ((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦)) |
4 | 1, 3 | sylan2 491 |
. . 3
⊢ ((𝐴 ∈ FinII ∧
𝑦 ∈ 𝒫
𝒫 𝐴) → ((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
→ ∩ 𝑦 ∈ 𝑦)) |
5 | 4 | ralrimiva 2966 |
. 2
⊢ (𝐴 ∈ FinII →
∀𝑦 ∈ 𝒫
𝒫 𝐴((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
→ ∩ 𝑦 ∈ 𝑦)) |
6 | | elpwi 4168 |
. . . . 5
⊢ (𝑏 ∈ 𝒫 𝒫
𝐴 → 𝑏 ⊆ 𝒫 𝐴) |
7 | | simp1r 1086 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ 𝑏 ⊆ 𝒫
𝐴) |
8 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴 |
9 | | simp1l 1085 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ 𝐴 ∈ 𝑉) |
10 | | pwexg 4850 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
11 | | elpw2g 4827 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∈
V → ({𝑐 ∈
𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴 ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴)) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ({𝑐 ∈ 𝒫
𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴 ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴)) |
13 | 8, 12 | mpbiri 248 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ {𝑐 ∈ 𝒫
𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴) |
14 | | simp2 1062 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∀𝑦 ∈
𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦)) |
15 | | simp3l 1089 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ 𝑏 ≠
∅) |
16 | | fin23lem7 9138 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ∧ 𝑏 ≠ ∅) → {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅) |
17 | 9, 7, 15, 16 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ {𝑐 ∈ 𝒫
𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅) |
18 | | sorpsscmpl 6948 |
. . . . . . . . . . . . 13
⊢ (
[⊊] Or 𝑏
→ [⊊] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
19 | 18 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ [⊊] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
20 | 19 | 3ad2ant3 1084 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ [⊊] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
21 | 17, 20 | jca 554 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ({𝑐 ∈ 𝒫
𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅ ∧ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
22 | | neeq1 2856 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → (𝑦 ≠ ∅ ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅)) |
23 | | soeq2 5055 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → ( [⊊] Or 𝑦 ↔ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
24 | 22, 23 | anbi12d 747 |
. . . . . . . . . . . 12
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → ((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) ↔ ({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅ ∧ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}))) |
25 | | inteq 4478 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → ∩ 𝑦 = ∩
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
26 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → 𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
27 | 25, 26 | eleq12d 2695 |
. . . . . . . . . . . 12
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → (∩ 𝑦 ∈ 𝑦 ↔ ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
28 | 24, 27 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} → (((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ↔ (({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅ ∧ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) → ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}))) |
29 | 28 | rspcv 3305 |
. . . . . . . . . 10
⊢ ({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴 → (∀𝑦 ∈ 𝒫 𝒫
𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) → (({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ≠ ∅ ∧ [⊊] Or
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) → ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}))) |
30 | 13, 14, 21, 29 | syl3c 66 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}) |
31 | | sorpssint 6947 |
. . . . . . . . . 10
⊢ (
[⊊] Or {𝑐
∈ 𝒫 𝐴 ∣
(𝐴 ∖ 𝑐) ∈ 𝑏} → (∃𝑧 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ¬ 𝑤 ⊊ 𝑧 ↔ ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
32 | 20, 31 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ (∃𝑧 ∈
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ¬ 𝑤 ⊊ 𝑧 ↔ ∩ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏})) |
33 | 30, 32 | mpbird 247 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∃𝑧 ∈
{𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ¬ 𝑤 ⊊ 𝑧) |
34 | | psseq1 3694 |
. . . . . . . . 9
⊢ (𝑚 = (𝐴 ∖ 𝑧) → (𝑚 ⊊ 𝑛 ↔ (𝐴 ∖ 𝑧) ⊊ 𝑛)) |
35 | | psseq1 3694 |
. . . . . . . . 9
⊢ (𝑤 = (𝐴 ∖ 𝑛) → (𝑤 ⊊ 𝑧 ↔ (𝐴 ∖ 𝑛) ⊊ 𝑧)) |
36 | | pssdifcom1 4054 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐴) → ((𝐴 ∖ 𝑧) ⊊ 𝑛 ↔ (𝐴 ∖ 𝑛) ⊊ 𝑧)) |
37 | 34, 35, 36 | fin23lem11 9139 |
. . . . . . . 8
⊢ (𝑏 ⊆ 𝒫 𝐴 → (∃𝑧 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝑏} ¬ 𝑤 ⊊ 𝑧 → ∃𝑚 ∈ 𝑏 ∀𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛)) |
38 | 7, 33, 37 | sylc 65 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∃𝑚 ∈
𝑏 ∀𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛) |
39 | | simp3r 1090 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ [⊊] Or 𝑏) |
40 | | sorpssuni 6946 |
. . . . . . . 8
⊢ (
[⊊] Or 𝑏
→ (∃𝑚 ∈
𝑏 ∀𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛 ↔ ∪ 𝑏 ∈ 𝑏)) |
41 | 39, 40 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ (∃𝑚 ∈
𝑏 ∀𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛 ↔ ∪ 𝑏 ∈ 𝑏)) |
42 | 38, 41 | mpbid 222 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) ∧ (𝑏 ≠ ∅ ∧
[⊊] Or 𝑏))
→ ∪ 𝑏 ∈ 𝑏) |
43 | 42 | 3exp 1264 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴) → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) → ((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ ∪ 𝑏 ∈ 𝑏))) |
44 | 6, 43 | sylan2 491 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝒫 𝒫 𝐴) → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) → ((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ ∪ 𝑏 ∈ 𝑏))) |
45 | 44 | ralrimdva 2969 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) →
∀𝑏 ∈ 𝒫
𝒫 𝐴((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ ∪ 𝑏 ∈ 𝑏))) |
46 | | isfin2 9116 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinII ↔
∀𝑏 ∈ 𝒫
𝒫 𝐴((𝑏 ≠ ∅ ∧
[⊊] Or 𝑏)
→ ∪ 𝑏 ∈ 𝑏))) |
47 | 45, 46 | sylibrd 249 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∩ 𝑦
∈ 𝑦) → 𝐴 ∈
FinII)) |
48 | 5, 47 | impbid2 216 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinII ↔
∀𝑦 ∈ 𝒫
𝒫 𝐴((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
→ ∩ 𝑦 ∈ 𝑦))) |