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 𝑌 → ( ∃ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∩ 𝑌 ∈ 𝑌 ) )