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	syl5bi	⊢ ( ( ( 𝑅 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	syl5bi	⊢ ( ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) → ( ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
52	51	expimpd	⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
53	52	reximdva	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
54	28 53	syl5bi	⊢ ( ( ( 𝑅 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	syl5bi	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
60	59	impr	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )