Proof of Theorem sorpssuni
Step | Hyp | Ref
| Expression |
1 | | sorpssi 7517 |
. . . . . . . . . 10
⊢ ((
[⊊] Or 𝑌
∧ (𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌)) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
2 | 1 | anassrs 471 |
. . . . . . . . 9
⊢ (((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) ∧ 𝑣 ∈ 𝑌) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
3 | | sspss 4014 |
. . . . . . . . . . 11
⊢ (𝑢 ⊆ 𝑣 ↔ (𝑢 ⊊ 𝑣 ∨ 𝑢 = 𝑣)) |
4 | | orel1 889 |
. . . . . . . . . . . 12
⊢ (¬
𝑢 ⊊ 𝑣 → ((𝑢 ⊊ 𝑣 ∨ 𝑢 = 𝑣) → 𝑢 = 𝑣)) |
5 | | eqimss2 3958 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → 𝑣 ⊆ 𝑢) |
6 | 4, 5 | syl6com 37 |
. . . . . . . . . . 11
⊢ ((𝑢 ⊊ 𝑣 ∨ 𝑢 = 𝑣) → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) |
7 | 3, 6 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝑢 ⊆ 𝑣 → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) |
8 | | ax-1 6 |
. . . . . . . . . 10
⊢ (𝑣 ⊆ 𝑢 → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) |
9 | 7, 8 | jaoi 857 |
. . . . . . . . 9
⊢ ((𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) |
10 | 2, 9 | syl 17 |
. . . . . . . 8
⊢ (((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) ∧ 𝑣 ∈ 𝑌) → (¬ 𝑢 ⊊ 𝑣 → 𝑣 ⊆ 𝑢)) |
11 | 10 | ralimdva 3100 |
. . . . . . 7
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) → (∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 → ∀𝑣 ∈ 𝑌 𝑣 ⊆ 𝑢)) |
12 | 11 | 3impia 1119 |
. . . . . 6
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → ∀𝑣 ∈ 𝑌 𝑣 ⊆ 𝑢) |
13 | | unissb 4853 |
. . . . . 6
⊢ (∪ 𝑌
⊆ 𝑢 ↔
∀𝑣 ∈ 𝑌 𝑣 ⊆ 𝑢) |
14 | 12, 13 | sylibr 237 |
. . . . 5
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → ∪ 𝑌 ⊆ 𝑢) |
15 | | elssuni 4851 |
. . . . . 6
⊢ (𝑢 ∈ 𝑌 → 𝑢 ⊆ ∪ 𝑌) |
16 | 15 | 3ad2ant2 1136 |
. . . . 5
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → 𝑢 ⊆ ∪ 𝑌) |
17 | 14, 16 | eqssd 3918 |
. . . 4
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → ∪ 𝑌 = 𝑢) |
18 | | simp2 1139 |
. . . 4
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → 𝑢 ∈ 𝑌) |
19 | 17, 18 | eqeltrd 2838 |
. . 3
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) → ∪ 𝑌 ∈ 𝑌) |
20 | 19 | rexlimdv3a 3205 |
. 2
⊢ (
[⊊] Or 𝑌
→ (∃𝑢 ∈
𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 → ∪ 𝑌 ∈ 𝑌)) |
21 | | elssuni 4851 |
. . . . 5
⊢ (𝑣 ∈ 𝑌 → 𝑣 ⊆ ∪ 𝑌) |
22 | | ssnpss 4018 |
. . . . 5
⊢ (𝑣 ⊆ ∪ 𝑌
→ ¬ ∪ 𝑌 ⊊ 𝑣) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝑣 ∈ 𝑌 → ¬ ∪
𝑌 ⊊ 𝑣) |
24 | 23 | rgen 3071 |
. . 3
⊢
∀𝑣 ∈
𝑌 ¬ ∪ 𝑌
⊊ 𝑣 |
25 | | psseq1 4002 |
. . . . . 6
⊢ (𝑢 = ∪
𝑌 → (𝑢 ⊊ 𝑣 ↔ ∪ 𝑌 ⊊ 𝑣)) |
26 | 25 | notbid 321 |
. . . . 5
⊢ (𝑢 = ∪
𝑌 → (¬ 𝑢 ⊊ 𝑣 ↔ ¬ ∪
𝑌 ⊊ 𝑣)) |
27 | 26 | ralbidv 3118 |
. . . 4
⊢ (𝑢 = ∪
𝑌 → (∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 ↔ ∀𝑣 ∈ 𝑌 ¬ ∪ 𝑌 ⊊ 𝑣)) |
28 | 27 | rspcev 3537 |
. . 3
⊢ ((∪ 𝑌
∈ 𝑌 ∧
∀𝑣 ∈ 𝑌 ¬ ∪ 𝑌
⊊ 𝑣) →
∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) |
29 | 24, 28 | mpan2 691 |
. 2
⊢ (∪ 𝑌
∈ 𝑌 →
∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣) |
30 | 20, 29 | impbid1 228 |
1
⊢ (
[⊊] Or 𝑌
→ (∃𝑢 ∈
𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 ↔ ∪ 𝑌 ∈ 𝑌)) |