Proof of Theorem sorpssuni
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sorpssi 7749 | . . . . . . . . . 10
⊢ ((
[⊊] Or 𝑌
∧ (𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌)) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) | 
| 2 | 1 | anassrs 467 | . . . . . . . . 9
⊢ (((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) ∧ 𝑣 ∈ 𝑌) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) | 
| 3 |  | sspss 4102 | . . . . . . . . . . 11
⊢ (𝑢 ⊆ 𝑣 ↔ (𝑢 ⊊ 𝑣 ∨ 𝑢 = 𝑣)) | 
| 4 |  | orel1 889 | . . . . . . . . . . . 12
⊢ (¬
𝑢 ⊊ 𝑣 → ((𝑢 ⊊ 𝑣 ∨ 𝑢 = 𝑣) → 𝑢 = 𝑣)) | 
| 5 |  | eqimss2 4043 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → 𝑣 ⊆ 𝑢) | 
| 6 | 4, 5 | syl6com 37 | . . . . . . . . . . 11
⊢ ((𝑢 ⊊ 𝑣 ∨ 𝑢 = 𝑣) → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) | 
| 7 | 3, 6 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑢 ⊆ 𝑣 → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) | 
| 8 |  | ax-1 6 | . . . . . . . . . 10
⊢ (𝑣 ⊆ 𝑢 → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) | 
| 9 | 7, 8 | jaoi 858 | . . . . . . . . 9
⊢ ((𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) | 
| 10 | 2, 9 | syl 17 | . . . . . . . 8
⊢ (((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) ∧ 𝑣 ∈ 𝑌) → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) | 
| 11 | 10 | ralimdva 3167 | . . . . . . 7
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) → (∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 → ∀𝑣 ∈ 𝑌 𝑣 ⊆ 𝑢)) | 
| 12 | 11 | 3impia 1118 | . . . . . 6
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → ∀𝑣 ∈ 𝑌 𝑣 ⊆ 𝑢) | 
| 13 |  | unissb 4939 | . . . . . 6
⊢ (∪ 𝑌
⊆ 𝑢 ↔
∀𝑣 ∈ 𝑌 𝑣 ⊆ 𝑢) | 
| 14 | 12, 13 | sylibr 234 | . . . . 5
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → ∪ 𝑌 ⊆ 𝑢) | 
| 15 |  | elssuni 4937 | . . . . . 6
⊢ (𝑢 ∈ 𝑌 → 𝑢 ⊆ ∪ 𝑌) | 
| 16 | 15 | 3ad2ant2 1135 | . . . . 5
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → 𝑢 ⊆ ∪ 𝑌) | 
| 17 | 14, 16 | eqssd 4001 | . . . 4
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → ∪ 𝑌 = 𝑢) | 
| 18 |  | simp2 1138 | . . . 4
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → 𝑢 ∈ 𝑌) | 
| 19 | 17, 18 | eqeltrd 2841 | . . 3
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → ∪ 𝑌 ∈ 𝑌) | 
| 20 | 19 | rexlimdv3a 3159 | . 2
⊢ (
[⊊] Or 𝑌
→ (∃𝑢 ∈
𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 → ∪ 𝑌 ∈ 𝑌)) | 
| 21 |  | elssuni 4937 | . . . . 5
⊢ (𝑣 ∈ 𝑌 → 𝑣 ⊆ ∪ 𝑌) | 
| 22 |  | ssnpss 4106 | . . . . 5
⊢ (𝑣 ⊆ ∪ 𝑌
→ ¬ ∪ 𝑌 ⊊ 𝑣) | 
| 23 | 21, 22 | syl 17 | . . . 4
⊢ (𝑣 ∈ 𝑌 → ¬ ∪
𝑌 ⊊ 𝑣) | 
| 24 | 23 | rgen 3063 | . . 3
⊢
∀𝑣 ∈
𝑌 ¬ ∪ 𝑌
⊊ 𝑣 | 
| 25 |  | psseq1 4090 | . . . . . 6
⊢ (𝑢 = ∪
𝑌 → (𝑢 ⊊ 𝑣 ↔ ∪ 𝑌 ⊊ 𝑣)) | 
| 26 | 25 | notbid 318 | . . . . 5
⊢ (𝑢 = ∪
𝑌 → (¬ 𝑢 ⊊ 𝑣 ↔ ¬ ∪
𝑌 ⊊ 𝑣)) | 
| 27 | 26 | ralbidv 3178 | . . . 4
⊢ (𝑢 = ∪
𝑌 → (∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 ↔ ∀𝑣 ∈ 𝑌 ¬ ∪ 𝑌 ⊊ 𝑣)) | 
| 28 | 27 | rspcev 3622 | . . 3
⊢ ((∪ 𝑌
∈ 𝑌 ∧
∀𝑣 ∈ 𝑌 ¬ ∪ 𝑌
⊊ 𝑣) →
∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) | 
| 29 | 24, 28 | mpan2 691 | . 2
⊢ (∪ 𝑌
∈ 𝑌 →
∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) | 
| 30 | 20, 29 | impbid1 225 | 1
⊢ (
[⊊] Or 𝑌
→ (∃𝑢 ∈
𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 ↔ ∪ 𝑌 ∈ 𝑌)) |