Metamath Proof Explorer

Theorem fisupcl

Description: A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011)

Ref Expression
Assertion fisupcl ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→supBAR∈B

Proof

Step Hyp Ref Expression
1 simpl ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→ROrA
2 1 supval2 ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
3 simpr3 ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→B⊆A
4 breq2 ⊢z=x→yRz↔yRx
5 4 rspcev ⊢x∈B∧yRx→∃z∈ByRz
6 5 ex ⊢x∈B→yRx→∃z∈ByRz
7 6 ralrimivw ⊢x∈B→∀y∈AyRx→∃z∈ByRz
8 7 a1d ⊢x∈B→∀y∈ByRx→∃z∈ByRz→∀y∈AyRx→∃z∈ByRz
9 8 anim2d ⊢x∈B→∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz→∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
10 9 rgen ⊢∀x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz→∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
11 10 a1i ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∀x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz→∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
12 soss ⊢B⊆A→ROrA→ROrB
13 3 1 12 sylc ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→ROrB
14 simpr1 ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→B∈Fin
15 simpr2 ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→B≠∅
16 fisupg ⊢ROrB∧B∈Fin∧B≠∅→∃x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
17 13 14 15 16 syl3anc ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∃x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
18 fisup2g ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∃x∈B∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
19 ssrexv ⊢B⊆A→∃x∈B∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
20 3 18 19 sylc ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
21 1 20 supeu ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
22 riotass2 ⊢B⊆A∧∀x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz→∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz∧∃x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz∧∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→ιx∈B|∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
23 3 11 17 21 22 syl22anc ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→ιx∈B|∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
24 13 17 supeu ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∃!x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
25 riotacl ⊢∃!x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz→ιx∈B|∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz∈B
26 24 25 syl ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→ιx∈B|∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz∈B
27 23 26 eqeltrrd ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz∈B
28 2 27 eqeltrd ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→supBAR∈B