Theorem sorpssuni

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

	Ref	Expression
Assertion	sorpssuni	⊢ ( [⊊] Or 𝑌 → ( ∃ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 ↔ ∪ 𝑌 ∈ 𝑌 ) )

Proof

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