Theorem infmo

Description: Any class B has at most one infimum in A (where R is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020)

	Ref	Expression
Hypothesis	infmo.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion	infmo	⊢ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		infmo.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		ancom	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
3	2	anbi2ci	⊢ ( ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) ↔ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) )
4		an42	⊢ ( ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) ↔ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
5		an42	⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ) ↔ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) )
6	3 4 5	3bitr4i	⊢ ( ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) ↔ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ) )
7		ralnex	⊢ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ¬ ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑥 )
8		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝑤 𝑅 𝑦 ↔ 𝑤 𝑅 𝑥 ) )
9		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 𝑥 ) )
10	9	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑥 ) )
11	8 10	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ↔ ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑥 ) ) )
12	11	rspcva	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑥 ) )
13		breq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑧 𝑅 𝑥 ) )
14	13	cbvrexvw	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑥 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑥 )
15	12 14	syl6ibr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( 𝑤 𝑅 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑥 ) )
16	15	con3d	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( ¬ ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑥 → ¬ 𝑤 𝑅 𝑥 ) )
17	7 16	syl5bi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 → ¬ 𝑤 𝑅 𝑥 ) )
18	17	expimpd	⊢ ( 𝑥 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑤 𝑅 𝑥 ) )
19	18	ad2antrl	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑤 𝑅 𝑥 ) )
20		ralnex	⊢ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ↔ ¬ ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑤 )
21		breq2	⊢ ( 𝑦 = 𝑤 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑤 ) )
22		breq2	⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 𝑤 ) )
23	22	rexbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑤 ) )
24	21 23	imbi12d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ↔ ( 𝑥 𝑅 𝑤 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑤 ) ) )
25	24	rspcva	⊢ ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( 𝑥 𝑅 𝑤 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑤 ) )
26		breq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝑅 𝑤 ↔ 𝑧 𝑅 𝑤 ) )
27	26	cbvrexvw	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑤 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑤 )
28	25 27	syl6ibr	⊢ ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( 𝑥 𝑅 𝑤 → ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑤 ) )
29	28	con3d	⊢ ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( ¬ ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑤 → ¬ 𝑥 𝑅 𝑤 ) )
30	20 29	syl5bi	⊢ ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 → ¬ 𝑥 𝑅 𝑤 ) )
31	30	expimpd	⊢ ( 𝑤 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) → ¬ 𝑥 𝑅 𝑤 ) )
32	31	ad2antll	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) → ¬ 𝑥 𝑅 𝑤 ) )
33	19 32	anim12d	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ) → ( ¬ 𝑤 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝑤 ) ) )
34	33	imp	⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ) ) → ( ¬ 𝑤 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝑤 ) )
35	34	ancomd	⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ) ) → ( ¬ 𝑥 𝑅 𝑤 ∧ ¬ 𝑤 𝑅 𝑥 ) )
36	35	ex	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) ) → ( ¬ 𝑥 𝑅 𝑤 ∧ ¬ 𝑤 𝑅 𝑥 ) ) )
37	6 36	syl5bi	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → ( ¬ 𝑥 𝑅 𝑤 ∧ ¬ 𝑤 𝑅 𝑥 ) ) )
38		sotrieq2	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑥 = 𝑤 ↔ ( ¬ 𝑥 𝑅 𝑤 ∧ ¬ 𝑤 𝑅 𝑥 ) ) )
39	37 38	sylibrd	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → 𝑥 = 𝑤 ) )
40	39	ralrimivva	⊢ ( 𝑅 Or 𝐴 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → 𝑥 = 𝑤 ) )
41	1 40	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → 𝑥 = 𝑤 ) )
42		breq2	⊢ ( 𝑥 = 𝑤 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑤 ) )
43	42	notbid	⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑤 ) )
44	43	ralbidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ) )
45		breq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝑅 𝑦 ↔ 𝑤 𝑅 𝑦 ) )
46	45	imbi1d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ↔ ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
47	46	ralbidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
48	44 47	anbi12d	⊢ ( 𝑥 = 𝑤 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
49	48	rmo4	⊢ ( ∃* 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → 𝑥 = 𝑤 ) )
50	41 49	sylibr	⊢ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )