Metamath Proof Explorer

Theorem wereu2

Description: A nonempty subclass of an R -well-ordered and R -setlike class has a unique R -minimal element. Proposition 6.26 of TakeutiZaring p. 31. (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion wereu2 ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐵 )
2 rabeq0 ⊢ ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } = ∅ ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 )
3 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑥 ↔ 𝑤 𝑅 𝑥 ) )
4 3 notbid ⊢ ( 𝑦 = 𝑤 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑤 𝑅 𝑥 ) )
5 4 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑥 )
6 breq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑤 𝑅 𝑥 ↔ 𝑤 𝑅 𝑧 ) )
7 6 notbid ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑤 𝑅 𝑥 ↔ ¬ 𝑤 𝑅 𝑧 ) )
8 7 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑥 ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 ) )
9 5 8 syl5bb ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 ) )
10 9 rspcev ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
11 10 ex ⊢ ( 𝑧 ∈ 𝐵 → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
12 11 ad2antll ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
13 2 12 syl5bi ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } = ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
14 simprl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐵 ⊆ 𝐴 )
15 simplr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Se 𝐴 )
16 sess2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Se 𝐴 → 𝑅 Se 𝐵 ) )
17 14 15 16 sylc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Se 𝐵 )
18 simprr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
19 seex ⊢ ( ( 𝑅 Se 𝐵 ∧ 𝑧 ∈ 𝐵 ) → { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∈ V )
20 17 18 19 syl2anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∈ V )
21 wefr ⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 )
22 21 ad2antrr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Fr 𝐴 )
23 ssrab2 ⊢ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ⊆ 𝐵
24 23 14 sstrid ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ⊆ 𝐴 )
25 fri ⊢ ( ( ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ⊆ 𝐴 ∧ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ≠ ∅ ) ) → ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 )
26 25 expr ⊢ ( ( ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ⊆ 𝐴 ) → ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
27 20 22 24 26 syl21anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
28 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝑅 𝑧 ↔ 𝑥 𝑅 𝑧 ) )
29 28 rexrab ⊢ ( ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
30 breq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 𝑅 𝑧 ↔ 𝑦 𝑅 𝑧 ) )
31 30 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) )
32 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
33 32 ad2antrr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Or 𝐴 )
34 soss ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Or 𝐴 → 𝑅 Or 𝐵 ) )
35 14 33 34 sylc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Or 𝐵 )
36 35 ad2antrr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑅 Or 𝐵 )
37 simpr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
38 simplr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
39 18 ad2antrr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
40 sotr ⊢ ( ( 𝑅 Or 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 𝑅 𝑥 ∧ 𝑥 𝑅 𝑧 ) → 𝑦 𝑅 𝑧 ) )
41 36 37 38 39 40 syl13anc ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 𝑅 𝑥 ∧ 𝑥 𝑅 𝑧 ) → 𝑦 𝑅 𝑧 ) )
42 41 ancomsd ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 𝑅 𝑧 ) )
43 42 expdimp ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) → ( 𝑦 𝑅 𝑥 → 𝑦 𝑅 𝑧 ) )
44 43 an32s ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 𝑅 𝑥 → 𝑦 𝑅 𝑧 ) )
45 44 con3d ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) )
46 idd ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑦 𝑅 𝑥 → ¬ 𝑦 𝑅 𝑥 ) )
47 45 46 jad ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑦 𝑅 𝑥 ) )
48 47 ralimdva ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
49 31 48 syl5bi ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) → ( ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
50 49 expimpd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
51 50 reximdva ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
52 29 51 syl5bi ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
53 27 52 syld ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
54 13 53 pm2.61dne ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
55 54 expr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
56 55 exlimdv ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑧 𝑧 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
57 1 56 syl5bi ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
58 57 impr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
59 simprl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → 𝐵 ⊆ 𝐴 )
60 32 ad2antrr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → 𝑅 Or 𝐴 )
61 59 60 34 sylc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → 𝑅 Or 𝐵 )
62 somo ⊢ ( 𝑅 Or 𝐵 → ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
63 61 62 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
64 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
65 58 63 64 sylanbrc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )