This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sorpssint

Description: In a chain of sets, a minimal element is the intersection of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion sorpssint ( [⊊] Or 𝑌 → ( ∃ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∩ 𝑌 ∈ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 intss1 ⊢ ( 𝑢 ∈ 𝑌 → ∩ 𝑌 ⊆ 𝑢 )
2 1 3ad2ant2 ⊢ ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ) → ∩ 𝑌 ⊆ 𝑢 )
3 sorpssi ⊢ ( ( [⊊] Or 𝑌 ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
4 3 anassrs ⊢ ( ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ) ∧ 𝑣 ∈ 𝑌 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
5 sspss ⊢ ( 𝑣 ⊆ 𝑢 ↔ ( 𝑣 ⊊ 𝑢 ∨ 𝑣 = 𝑢 ) )
6 orel1 ⊢ ( ¬ 𝑣 ⊊ 𝑢 → ( ( 𝑣 ⊊ 𝑢 ∨ 𝑣 = 𝑢 ) → 𝑣 = 𝑢 ) )
7 eqimss2 ⊢ ( 𝑣 = 𝑢 → 𝑢 ⊆ 𝑣 )
8 6 7 syl6com ⊢ ( ( 𝑣 ⊊ 𝑢 ∨ 𝑣 = 𝑢 ) → ( ¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣 ) )
9 5 8 sylbi ⊢ ( 𝑣 ⊆ 𝑢 → ( ¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣 ) )
10 9 jao1i ⊢ ( ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) → ( ¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣 ) )
11 4 10 syl ⊢ ( ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ) ∧ 𝑣 ∈ 𝑌 ) → ( ¬ 𝑣 ⊊ 𝑢 → 𝑢 ⊆ 𝑣 ) )
12 11 ralimdva ⊢ ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ) → ( ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 → ∀ 𝑣 ∈ 𝑌 𝑢 ⊆ 𝑣 ) )
13 12 3impia ⊢ ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ) → ∀ 𝑣 ∈ 𝑌 𝑢 ⊆ 𝑣 )
14 ssint ⊢ ( 𝑢 ⊆ ∩ 𝑌 ↔ ∀ 𝑣 ∈ 𝑌 𝑢 ⊆ 𝑣 )
15 13 14 sylibr ⊢ ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ) → 𝑢 ⊆ ∩ 𝑌 )
16 2 15 eqssd ⊢ ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ) → ∩ 𝑌 = 𝑢 )
17 simp2 ⊢ ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ) → 𝑢 ∈ 𝑌 )
18 16 17 eqeltrd ⊢ ( ( [⊊] Or 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ) → ∩ 𝑌 ∈ 𝑌 )
19 18 rexlimdv3a ⊢ ( [⊊] Or 𝑌 → ( ∃ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 → ∩ 𝑌 ∈ 𝑌 ) )
20 intss1 ⊢ ( 𝑣 ∈ 𝑌 → ∩ 𝑌 ⊆ 𝑣 )
21 ssnpss ⊢ ( ∩ 𝑌 ⊆ 𝑣 → ¬ 𝑣 ⊊ ∩ 𝑌 )
22 20 21 syl ⊢ ( 𝑣 ∈ 𝑌 → ¬ 𝑣 ⊊ ∩ 𝑌 )
23 22 rgen ⊢ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ ∩ 𝑌
24 psseq2 ⊢ ( 𝑢 = ∩ 𝑌 → ( 𝑣 ⊊ 𝑢 ↔ 𝑣 ⊊ ∩ 𝑌 ) )
25 24 notbid ⊢ ( 𝑢 = ∩ 𝑌 → ( ¬ 𝑣 ⊊ 𝑢 ↔ ¬ 𝑣 ⊊ ∩ 𝑌 ) )
26 25 ralbidv ⊢ ( 𝑢 = ∩ 𝑌 → ( ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ ∩ 𝑌 ) )
27 26 rspcev ⊢ ( ( ∩ 𝑌 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ ∩ 𝑌 ) → ∃ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 )
28 23 27 mpan2 ⊢ ( ∩ 𝑌 ∈ 𝑌 → ∃ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 )
29 19 28 impbid1 ⊢ ( [⊊] Or 𝑌 → ( ∃ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∩ 𝑌 ∈ 𝑌 ) )