Theorem frpomin 6343

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

Assertion

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

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝑅,𝑦   𝑥,𝐵,𝑦

Proof of Theorem frpomin

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0 4299	. . 3 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐵)
2		rabeq0 4337	. . . . . . 7 ⊢ ({𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} = ∅ ↔ ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧)
3		simprr 785	. . . . . . . 8 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵)
4		breq1 5105	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (𝑦𝑅𝑥 ↔ 𝑤𝑅𝑥))
5	4	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
6	5	cbvralvw 3240	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑥)
7		breq2 5106	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑤𝑅𝑥 ↔ 𝑤𝑅𝑧))
8	7	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (¬ 𝑤𝑅𝑥 ↔ ¬ 𝑤𝑅𝑧))
9	8	ralbidv 3185	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑥 ↔ ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧))
10	6, 9	bitrid 286	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧))
11	10	rspcev 3576	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
12	11	ex 418	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
13	3, 12	syl 18	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
14	2, 13	biimtrid 245	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ({𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} = ∅ → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
15		simprl 783	. . . . . . . . . 10 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝐵 ⊆ 𝐴)
16		simpl3 1212	. . . . . . . . . 10 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑅 Se 𝐴)
17		sess2 5616	. . . . . . . . . 10 ⊢ (𝐵 ⊆ 𝐴 → (𝑅 Se 𝐴 → 𝑅 Se 𝐵))
18	15, 16, 17	sylc 66	. . . . . . . . 9 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑅 Se 𝐵)
19		seex 5609	. . . . . . . . 9 ⊢ ((𝑅 Se 𝐵 ∧ 𝑧 ∈ 𝐵) → {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ∈ V)
20	18, 3, 19	syl2anc 596	. . . . . . . 8 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ∈ V)
21		simpl1 1210	. . . . . . . 8 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑅 Fr 𝐴)
22		ssrab2 4005	. . . . . . . . 9 ⊢ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ⊆ 𝐵
23	22, 15	sstrid 3919	. . . . . . . 8 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ⊆ 𝐴)
24		fri 5608	. . . . . . . . 9 ⊢ ((({𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ⊆ 𝐴 ∧ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ≠ ∅)) → ∃𝑥 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧}∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥)
25	24	expr 462	. . . . . . . 8 ⊢ ((({𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ⊆ 𝐴) → ({𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧}∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
26	20, 21, 23, 25	syl21anc 851	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ({𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧}∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
27		breq1 5105	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑤𝑅𝑧 ↔ 𝑥𝑅𝑧))
28	27	rexrab 3653	. . . . . . . 8 ⊢ (∃𝑥 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧}∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∃𝑥 ∈ 𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
29		breq1 5105	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑦 → (𝑤𝑅𝑧 ↔ 𝑦𝑅𝑧))
30	29	ralrab 3651	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
31		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝑦𝑅𝑥)
32		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝑥𝑅𝑧)
33		simplrl 789	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) → 𝐵 ⊆ 𝐴)
34	33	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝐵 ⊆ 𝐴)
35		simpll2 1232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) → 𝑅 Po 𝐴)
36	35	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝑅 Po 𝐴)
37		poss 5560	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ⊆ 𝐴 → (𝑅 Po 𝐴 → 𝑅 Po 𝐵))
38	34, 36, 37	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝑅 Po 𝐵)
39		simprl 783	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝑦 ∈ 𝐵)
40		simpllr 788	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝑥 ∈ 𝐵)
41		simplrr 790	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) → 𝑧 ∈ 𝐵)
42	41	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝑧 ∈ 𝐵)
43		potr 5571	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Po 𝐵 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦𝑅𝑥 ∧ 𝑥𝑅𝑧) → 𝑦𝑅𝑧))
44	38, 39, 40, 42, 43	syl13anc 1399	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → ((𝑦𝑅𝑥 ∧ 𝑥𝑅𝑧) → 𝑦𝑅𝑧))
45	31, 32, 44	mp2and 712	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) → 𝑦𝑅𝑧)
46	45	expr 462	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦 ∈ 𝐵) → (𝑦𝑅𝑥 → 𝑦𝑅𝑧))
47	46	con3d 153	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦 ∈ 𝐵) → (¬ 𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
48		idd 25	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦 ∈ 𝐵) → (¬ 𝑦𝑅𝑥 → ¬ 𝑦𝑅𝑥))
49	47, 48	jad 189	. . . . . . . . . . . 12 ⊢ ((((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦 ∈ 𝐵) → ((𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥))
50	49	ralimdva 3174	. . . . . . . . . . 11 ⊢ (((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦 ∈ 𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
51	30, 50	biimtrid 245	. . . . . . . . . 10 ⊢ (((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
52	51	expimpd 459	. . . . . . . . 9 ⊢ ((((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐵) → ((𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
53	52	reximdva 3175	. . . . . . . 8 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (∃𝑥 ∈ 𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
54	28, 53	biimtrid 245	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (∃𝑥 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧}∀𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
55	26, 54	syld 48	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ({𝑤 ∈ 𝐵 ∣ 𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
56	14, 55	pm2.61dne 3041	. . . . 5 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
57	56	expr 462	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ⊆ 𝐴) → (𝑧 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
58	57	exlimdv 1965	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ⊆ 𝐴) → (∃𝑧 𝑧 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
59	1, 58	biimtrid 245	. 2 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ⊆ 𝐴) → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥))
60	59	impr 460	1 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895  ∅c0 4278   class class class wbr 5102   Po wpo 5556   Fr wfr 5600   Se wse 5601

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-po 5558  df-fr 5603  df-se 5604

This theorem is used by:  frpomin2  6344