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

Metamath Proof Explorer

Theorem frpomin

Description: Every nonempty (possibly proper) subclass of a class A with a well-founded set-like partial order R has a minimal element. The additional condition of partial order over frmin enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022)

Ref Expression
Assertion frpomin ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐵 )
2 rabeq0 ⊢ ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } = ∅ ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 )
3 simprr ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
4 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑥 ↔ 𝑤 𝑅 𝑥 ) )
5 4 notbid ⊢ ( 𝑦 = 𝑤 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑤 𝑅 𝑥 ) )
6 5 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑥 )
7 breq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑤 𝑅 𝑥 ↔ 𝑤 𝑅 𝑧 ) )
8 7 notbid ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑤 𝑅 𝑥 ↔ ¬ 𝑤 𝑅 𝑧 ) )
9 8 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑥 ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 ) )
10 6 9 bitrid ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 ) )
11 10 rspcev ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
12 11 ex ⊢ ( 𝑧 ∈ 𝐵 → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
13 3 12 syl ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
14 2 13 biimtrid ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } = ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
15 simprl ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐵 ⊆ 𝐴 )
16 simpl3 ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Se 𝐴 )
17 sess2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Se 𝐴 → 𝑅 Se 𝐵 ) )
18 15 16 17 sylc ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Se 𝐵 )
19 seex ⊢ ( ( 𝑅 Se 𝐵 ∧ 𝑧 ∈ 𝐵 ) → { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∈ V )
20 18 3 19 syl2anc ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∈ V )
21 simpl1 ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Fr 𝐴 )
22 ssrab2 ⊢ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ⊆ 𝐵
23 22 15 sstrid ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ⊆ 𝐴 )
24 fri ⊢ ( ( ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ⊆ 𝐴 ∧ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ≠ ∅ ) ) → ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 )
25 24 expr ⊢ ( ( ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ⊆ 𝐴 ) → ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
26 20 21 23 25 syl21anc ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
27 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝑅 𝑧 ↔ 𝑥 𝑅 𝑧 ) )
28 27 rexrab ⊢ ( ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
29 breq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 𝑅 𝑧 ↔ 𝑦 𝑅 𝑧 ) )
30 29 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) )
31 simprr ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑦 𝑅 𝑥 )
32 simplr ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑥 𝑅 𝑧 )
33 simplrl ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ⊆ 𝐴 )
34 33 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝐵 ⊆ 𝐴 )
35 simpll2 ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 Po 𝐴 )
36 35 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑅 Po 𝐴 )
37 poss ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Po 𝐴 → 𝑅 Po 𝐵 ) )
38 34 36 37 sylc ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑅 Po 𝐵 )
39 simprl ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑦 ∈ 𝐵 )
40 simpllr ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑥 ∈ 𝐵 )
41 simplrr ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
42 41 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑧 ∈ 𝐵 )
43 potr ⊢ ( ( 𝑅 Po 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 𝑅 𝑥 ∧ 𝑥 𝑅 𝑧 ) → 𝑦 𝑅 𝑧 ) )
44 38 39 40 42 43 syl13anc ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → ( ( 𝑦 𝑅 𝑥 ∧ 𝑥 𝑅 𝑧 ) → 𝑦 𝑅 𝑧 ) )
45 31 32 44 mp2and ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑦 𝑅 𝑧 )
46 45 expr ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 𝑅 𝑥 → 𝑦 𝑅 𝑧 ) )
47 46 con3d ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) )
48 idd ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑦 𝑅 𝑥 → ¬ 𝑦 𝑅 𝑥 ) )
49 47 48 jad ⊢ ( ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑦 𝑅 𝑥 ) )
50 49 ralimdva ⊢ ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
51 30 50 biimtrid ⊢ ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) → ( ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
52 51 expimpd ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
53 52 reximdva ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
54 28 53 biimtrid ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∃ 𝑥 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
55 26 54 syld ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
56 14 55 pm2.61dne ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
57 56 expr ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
58 57 exlimdv ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑧 𝑧 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
59 1 58 biimtrid ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
60 59 impr ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )