Step |
Hyp |
Ref |
Expression |
1 |
|
elpwi |
⊢ ( 𝑦 ∈ 𝒫 𝒫 𝐴 → 𝑦 ⊆ 𝒫 𝐴 ) |
2 |
|
fin2i2 |
⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝑦 ⊆ 𝒫 𝐴 ) ∧ ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) ) → ∩ 𝑦 ∈ 𝑦 ) |
3 |
2
|
ex |
⊢ ( ( 𝐴 ∈ FinII ∧ 𝑦 ⊆ 𝒫 𝐴 ) → ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ) |
4 |
1 3
|
sylan2 |
⊢ ( ( 𝐴 ∈ FinII ∧ 𝑦 ∈ 𝒫 𝒫 𝐴 ) → ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ) |
5 |
4
|
ralrimiva |
⊢ ( 𝐴 ∈ FinII → ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ) |
6 |
|
elpwi |
⊢ ( 𝑏 ∈ 𝒫 𝒫 𝐴 → 𝑏 ⊆ 𝒫 𝐴 ) |
7 |
|
simp1r |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → 𝑏 ⊆ 𝒫 𝐴 ) |
8 |
|
simp1l |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → 𝐴 ∈ 𝑉 ) |
9 |
|
simp3l |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → 𝑏 ≠ ∅ ) |
10 |
|
fin23lem7 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ∧ 𝑏 ≠ ∅ ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ≠ ∅ ) |
11 |
8 7 9 10
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ≠ ∅ ) |
12 |
|
sorpsscmpl |
⊢ ( [⊊] Or 𝑏 → [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) |
13 |
12
|
adantl |
⊢ ( ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) → [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) |
14 |
13
|
3ad2ant3 |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) |
15 |
|
neeq1 |
⊢ ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } → ( 𝑦 ≠ ∅ ↔ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ≠ ∅ ) ) |
16 |
|
soeq2 |
⊢ ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } → ( [⊊] Or 𝑦 ↔ [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) ) |
17 |
15 16
|
anbi12d |
⊢ ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } → ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) ↔ ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ≠ ∅ ∧ [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) ) ) |
18 |
|
inteq |
⊢ ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } → ∩ 𝑦 = ∩ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) |
19 |
|
id |
⊢ ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } → 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) |
20 |
18 19
|
eleq12d |
⊢ ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } → ( ∩ 𝑦 ∈ 𝑦 ↔ ∩ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) ) |
21 |
17 20
|
imbi12d |
⊢ ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } → ( ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ↔ ( ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ≠ ∅ ∧ [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) → ∩ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) ) ) |
22 |
|
simp2 |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ) |
23 |
|
ssrab2 |
⊢ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ⊆ 𝒫 𝐴 |
24 |
|
pwexg |
⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V ) |
25 |
|
elpw2g |
⊢ ( 𝒫 𝐴 ∈ V → ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ 𝒫 𝒫 𝐴 ↔ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ⊆ 𝒫 𝐴 ) ) |
26 |
8 24 25
|
3syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ 𝒫 𝒫 𝐴 ↔ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ⊆ 𝒫 𝐴 ) ) |
27 |
23 26
|
mpbiri |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ 𝒫 𝒫 𝐴 ) |
28 |
21 22 27
|
rspcdva |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ( ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ≠ ∅ ∧ [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) → ∩ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) ) |
29 |
11 14 28
|
mp2and |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ∩ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) |
30 |
|
sorpssint |
⊢ ( [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } → ( ∃ 𝑧 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ¬ 𝑤 ⊊ 𝑧 ↔ ∩ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) ) |
31 |
14 30
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ( ∃ 𝑧 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ¬ 𝑤 ⊊ 𝑧 ↔ ∩ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ) ) |
32 |
29 31
|
mpbird |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ∃ 𝑧 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ¬ 𝑤 ⊊ 𝑧 ) |
33 |
|
psseq1 |
⊢ ( 𝑚 = ( 𝐴 ∖ 𝑧 ) → ( 𝑚 ⊊ 𝑛 ↔ ( 𝐴 ∖ 𝑧 ) ⊊ 𝑛 ) ) |
34 |
|
psseq1 |
⊢ ( 𝑤 = ( 𝐴 ∖ 𝑛 ) → ( 𝑤 ⊊ 𝑧 ↔ ( 𝐴 ∖ 𝑛 ) ⊊ 𝑧 ) ) |
35 |
|
pssdifcom1 |
⊢ ( ( 𝑧 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐴 ) → ( ( 𝐴 ∖ 𝑧 ) ⊊ 𝑛 ↔ ( 𝐴 ∖ 𝑛 ) ⊊ 𝑧 ) ) |
36 |
33 34 35
|
fin23lem11 |
⊢ ( 𝑏 ⊆ 𝒫 𝐴 → ( ∃ 𝑧 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝑏 } ¬ 𝑤 ⊊ 𝑧 → ∃ 𝑚 ∈ 𝑏 ∀ 𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛 ) ) |
37 |
7 32 36
|
sylc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ∃ 𝑚 ∈ 𝑏 ∀ 𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛 ) |
38 |
|
simp3r |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → [⊊] Or 𝑏 ) |
39 |
|
sorpssuni |
⊢ ( [⊊] Or 𝑏 → ( ∃ 𝑚 ∈ 𝑏 ∀ 𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛 ↔ ∪ 𝑏 ∈ 𝑏 ) ) |
40 |
38 39
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ( ∃ 𝑚 ∈ 𝑏 ∀ 𝑛 ∈ 𝑏 ¬ 𝑚 ⊊ 𝑛 ↔ ∪ 𝑏 ∈ 𝑏 ) ) |
41 |
37 40
|
mpbid |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) ) → ∪ 𝑏 ∈ 𝑏 ) |
42 |
41
|
3exp |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝒫 𝐴 ) → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) → ( ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) → ∪ 𝑏 ∈ 𝑏 ) ) ) |
43 |
6 42
|
sylan2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝒫 𝒫 𝐴 ) → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) → ( ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) → ∪ 𝑏 ∈ 𝑏 ) ) ) |
44 |
43
|
ralrimdva |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) → ∀ 𝑏 ∈ 𝒫 𝒫 𝐴 ( ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) → ∪ 𝑏 ∈ 𝑏 ) ) ) |
45 |
|
isfin2 |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinII ↔ ∀ 𝑏 ∈ 𝒫 𝒫 𝐴 ( ( 𝑏 ≠ ∅ ∧ [⊊] Or 𝑏 ) → ∪ 𝑏 ∈ 𝑏 ) ) ) |
46 |
44 45
|
sylibrd |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) → 𝐴 ∈ FinII ) ) |
47 |
5 46
|
impbid2 |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinII ↔ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ) ) |