Proof of Theorem sorpssint
Step | Hyp | Ref
| Expression |
1 | | intss1 4492 |
. . . . . 6
⊢ (𝑢 ∈ 𝑌 → ∩ 𝑌 ⊆ 𝑢) |
2 | 1 | 3ad2ant2 1083 |
. . . . 5
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢) → ∩ 𝑌 ⊆ 𝑢) |
3 | | sorpssi 6943 |
. . . . . . . . . 10
⊢ ((
[⊊] Or 𝑌
∧ (𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌)) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
4 | 3 | anassrs 680 |
. . . . . . . . 9
⊢ (((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) ∧ 𝑣 ∈ 𝑌) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
5 | | ax-1 6 |
. . . . . . . . . 10
⊢ (𝑢 ⊆ 𝑣 → (¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣)) |
6 | | sspss 3706 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ 𝑢 ↔ (𝑣 ⊊ 𝑢 ∨ 𝑣 = 𝑢)) |
7 | | orel1 397 |
. . . . . . . . . . . 12
⊢ (¬
𝑣 ⊊ 𝑢 → ((𝑣 ⊊ 𝑢 ∨ 𝑣 = 𝑢) → 𝑣 = 𝑢)) |
8 | | eqimss2 3658 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑢 → 𝑢 ⊆ 𝑣) |
9 | 7, 8 | syl6com 37 |
. . . . . . . . . . 11
⊢ ((𝑣 ⊊ 𝑢 ∨ 𝑣 = 𝑢) → (¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣)) |
10 | 6, 9 | sylbi 207 |
. . . . . . . . . 10
⊢ (𝑣 ⊆ 𝑢 → (¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣)) |
11 | 5, 10 | jaoi 394 |
. . . . . . . . 9
⊢ ((𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) → (¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣)) |
12 | 4, 11 | syl 17 |
. . . . . . . 8
⊢ (((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) ∧ 𝑣 ∈ 𝑌) → (¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣)) |
13 | 12 | ralimdva 2962 |
. . . . . . 7
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌) → (∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 → ∀𝑣 ∈ 𝑌 𝑢 ⊆ 𝑣)) |
14 | 13 | 3impia 1261 |
. . . . . 6
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢) → ∀𝑣 ∈ 𝑌 𝑢 ⊆ 𝑣) |
15 | | ssint 4493 |
. . . . . 6
⊢ (𝑢 ⊆ ∩ 𝑌
↔ ∀𝑣 ∈
𝑌 𝑢 ⊆ 𝑣) |
16 | 14, 15 | sylibr 224 |
. . . . 5
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢) → 𝑢 ⊆ ∩ 𝑌) |
17 | 2, 16 | eqssd 3620 |
. . . 4
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢) → ∩ 𝑌 = 𝑢) |
18 | | simp2 1062 |
. . . 4
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢) → 𝑢 ∈ 𝑌) |
19 | 17, 18 | eqeltrd 2701 |
. . 3
⊢ ((
[⊊] Or 𝑌
∧ 𝑢 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢) → ∩ 𝑌 ∈ 𝑌) |
20 | 19 | rexlimdv3a 3033 |
. 2
⊢ (
[⊊] Or 𝑌
→ (∃𝑢 ∈
𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 → ∩ 𝑌 ∈ 𝑌)) |
21 | | intss1 4492 |
. . . . 5
⊢ (𝑣 ∈ 𝑌 → ∩ 𝑌 ⊆ 𝑣) |
22 | | ssnpss 3710 |
. . . . 5
⊢ (∩ 𝑌
⊆ 𝑣 → ¬
𝑣 ⊊ ∩ 𝑌) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝑣 ∈ 𝑌 → ¬ 𝑣 ⊊ ∩ 𝑌) |
24 | 23 | rgen 2922 |
. . 3
⊢
∀𝑣 ∈
𝑌 ¬ 𝑣 ⊊ ∩ 𝑌 |
25 | | psseq2 3695 |
. . . . . 6
⊢ (𝑢 = ∩
𝑌 → (𝑣 ⊊ 𝑢 ↔ 𝑣 ⊊ ∩ 𝑌)) |
26 | 25 | notbid 308 |
. . . . 5
⊢ (𝑢 = ∩
𝑌 → (¬ 𝑣 ⊊ 𝑢 ↔ ¬ 𝑣 ⊊ ∩ 𝑌)) |
27 | 26 | ralbidv 2986 |
. . . 4
⊢ (𝑢 = ∩
𝑌 → (∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ ∩ 𝑌)) |
28 | 27 | rspcev 3309 |
. . 3
⊢ ((∩ 𝑌
∈ 𝑌 ∧
∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ ∩ 𝑌) → ∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢) |
29 | 24, 28 | mpan2 707 |
. 2
⊢ (∩ 𝑌
∈ 𝑌 →
∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢) |
30 | 20, 29 | impbid1 215 |
1
⊢ (
[⊊] Or 𝑌
→ (∃𝑢 ∈
𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∩ 𝑌 ∈ 𝑌)) |