Metamath Proof Explorer

Theorem fisup2g

Description: A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fisup2g ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∃x∈B∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz

Proof

Step Hyp Ref Expression
1 soss ⊢B⊆A→ROrA→ROrB
2 simp1 ⊢ROrB∧B∈Fin∧B≠∅→ROrB
3 fisupg ⊢ROrB∧B∈Fin∧B≠∅→∃x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
4 2 3 supeu ⊢ROrB∧B∈Fin∧B≠∅→∃!x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
5 4 3exp ⊢ROrB→B∈Fin→B≠∅→∃!x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
6 1 5 syl6 ⊢B⊆A→ROrA→B∈Fin→B≠∅→∃!x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
7 6 com4l ⊢ROrA→B∈Fin→B≠∅→B⊆A→∃!x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
8 7 3imp2 ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∃!x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
9 reurex ⊢∃!x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz→∃x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz
10 breq2 ⊢z=x→yRz↔yRx
11 10 rspcev ⊢x∈B∧yRx→∃z∈ByRz
12 11 ex ⊢x∈B→yRx→∃z∈ByRz
13 12 ralrimivw ⊢x∈B→∀y∈AyRx→∃z∈ByRz
14 13 a1d ⊢x∈B→∀y∈ByRx→∃z∈ByRz→∀y∈AyRx→∃z∈ByRz
15 14 anim2d ⊢x∈B→∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz→∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
16 15 reximia ⊢∃x∈B∀y∈B¬xRy∧∀y∈ByRx→∃z∈ByRz→∃x∈B∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
17 8 9 16 3syl ⊢ROrA∧B∈Fin∧B≠∅∧B⊆A→∃x∈B∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz