Metamath Proof Explorer

Theorem sorpsscmpl

Description: The componentwise complement of a chain of sets is also a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion sorpsscmpl ( [⊊] Or 𝑌 → [⊊] Or { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } )

Proof

Step Hyp Ref Expression
1 difeq2 ⊢ ( 𝑢 = 𝑥 → ( 𝐴 ∖ 𝑢 ) = ( 𝐴 ∖ 𝑥 ) )
2 1 eleq1d ⊢ ( 𝑢 = 𝑥 → ( ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 ↔ ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ) )
3 2 elrab ⊢ ( 𝑥 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ) )
4 difeq2 ⊢ ( 𝑢 = 𝑦 → ( 𝐴 ∖ 𝑢 ) = ( 𝐴 ∖ 𝑦 ) )
5 4 eleq1d ⊢ ( 𝑢 = 𝑦 → ( ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 ↔ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) )
6 5 elrab ⊢ ( 𝑦 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) )
7 an4 ⊢ ( ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) ) ↔ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) ∧ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) ) )
8 7 biimpi ⊢ ( ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) ) → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) ∧ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) ) )
9 3 6 8 syl2anb ⊢ ( ( 𝑥 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ∧ 𝑦 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ) → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) ∧ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) ) )
10 sorpssi ⊢ ( ( [⊊] Or 𝑌 ∧ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) ) → ( ( 𝐴 ∖ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) ∨ ( 𝐴 ∖ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑥 ) ) )
11 10 expcom ⊢ ( ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) → ( [⊊] Or 𝑌 → ( ( 𝐴 ∖ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) ∨ ( 𝐴 ∖ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑥 ) ) ) )
12 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
13 dfss4 ⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 )
14 12 13 bitri ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 )
15 velpw ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
16 dfss4 ⊢ ( 𝑦 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 )
17 15 16 bitri ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 )
18 sscon ⊢ ( ( 𝐴 ∖ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑥 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) )
19 sseq12 ⊢ ( ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 ∧ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 ) → ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) ↔ 𝑥 ⊆ 𝑦 ) )
20 18 19 syl5ib ⊢ ( ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 ∧ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 ) → ( ( 𝐴 ∖ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑥 ) → 𝑥 ⊆ 𝑦 ) )
21 sscon ⊢ ( ( 𝐴 ∖ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) )
22 sseq12 ⊢ ( ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 ∧ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 ) → ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ↔ 𝑦 ⊆ 𝑥 ) )
23 22 ancoms ⊢ ( ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 ∧ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 ) → ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ↔ 𝑦 ⊆ 𝑥 ) )
24 21 23 syl5ib ⊢ ( ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 ∧ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 ) → ( ( 𝐴 ∖ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) → 𝑦 ⊆ 𝑥 ) )
25 20 24 orim12d ⊢ ( ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 ∧ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 ) → ( ( ( 𝐴 ∖ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑥 ) ∨ ( 𝐴 ∖ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ) )
26 14 17 25 syl2anb ⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) → ( ( ( 𝐴 ∖ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑥 ) ∨ ( 𝐴 ∖ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ) )
27 26 com12 ⊢ ( ( ( 𝐴 ∖ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑥 ) ∨ ( 𝐴 ∖ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) ) → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ) )
28 27 orcoms ⊢ ( ( ( 𝐴 ∖ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) ∨ ( 𝐴 ∖ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑥 ) ) → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ) )
29 11 28 syl6 ⊢ ( ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) → ( [⊊] Or 𝑌 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ) ) )
30 29 com3l ⊢ ( [⊊] Or 𝑌 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) → ( ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ) ) )
31 30 impd ⊢ ( [⊊] Or 𝑌 → ( ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ) ∧ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑌 ∧ ( 𝐴 ∖ 𝑦 ) ∈ 𝑌 ) ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ) )
32 9 31 syl5 ⊢ ( [⊊] Or 𝑌 → ( ( 𝑥 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ∧ 𝑦 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ) )
33 32 ralrimivv ⊢ ( [⊊] Or 𝑌 → ∀ 𝑥 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ∀ 𝑦 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )
34 sorpss ⊢ ( [⊊] Or { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ↔ ∀ 𝑥 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ∀ 𝑦 ∈ { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )
35 33 34 sylibr ⊢ ( [⊊] Or 𝑌 → [⊊] Or { 𝑢 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑢 ) ∈ 𝑌 } )