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

Metamath Proof Explorer

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