Theorem eqinf

Description: Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020)

	Ref	Expression
Hypothesis	infexd.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion	eqinf	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		infexd.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		df-inf	⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 )
3		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
4	1 3	sylib	⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 )
5	4	eqsup	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) = 𝐶 ) )
6		brcnvg	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑦 ∈ V ) → ( 𝐶 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝐶 ) )
7	6	bicomd	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑦 ∈ V ) → ( 𝑦 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 𝑦 ) )
8	7	elvd	⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 𝑦 ) )
9	8	notbid	⊢ ( 𝐶 ∈ 𝐴 → ( ¬ 𝑦 𝑅 𝐶 ↔ ¬ 𝐶 ◡ 𝑅 𝑦 ) )
10	9	ralbidv	⊢ ( 𝐶 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ) )
11		vex	⊢ 𝑦 ∈ V
12		brcnvg	⊢ ( ( 𝑦 ∈ V ∧ 𝐶 ∈ 𝐴 ) → ( 𝑦 ◡ 𝑅 𝐶 ↔ 𝐶 𝑅 𝑦 ) )
13	11 12	mpan	⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 ◡ 𝑅 𝐶 ↔ 𝐶 𝑅 𝑦 ) )
14	13	bicomd	⊢ ( 𝐶 ∈ 𝐴 → ( 𝐶 𝑅 𝑦 ↔ 𝑦 ◡ 𝑅 𝐶 ) )
15		vex	⊢ 𝑧 ∈ V
16	11 15	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 )
17	16	a1i	⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 ) )
18	17	bicomd	⊢ ( 𝐶 ∈ 𝐴 → ( 𝑧 𝑅 𝑦 ↔ 𝑦 ◡ 𝑅 𝑧 ) )
19	18	rexbidv	⊢ ( 𝐶 ∈ 𝐴 → ( ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) )
20	14 19	imbi12d	⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ↔ ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
21	20	ralbidv	⊢ ( 𝐶 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
22	10 21	anbi12d	⊢ ( 𝐶 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )
23	22	pm5.32i	⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )
24		3anass	⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
25		3anass	⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )
26	23 24 25	3bitr4i	⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
27	26	biimpi	⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
28	5 27	impel	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) = 𝐶 )
29	2 28	syl5eq	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 )
30	29	ex	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) )