weinflb

Description: In a well-order, an infimum is a lower bound. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Hypotheses	weinflb.1	⊢ ( 𝜑 → Rel 𝑅 )
	weinflb.2	⊢ ( 𝜑 → 𝑅 We 𝐴 )
	weinflb.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	weinflb.4	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
	weinflb.5	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
	weinflb.6	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion	weinflb	⊢ ( 𝜑 → ¬ 𝐶 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		weinflb.1	⊢ ( 𝜑 → Rel 𝑅 )
2		weinflb.2	⊢ ( 𝜑 → 𝑅 We 𝐴 )
3		weinflb.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		weinflb.4	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
5		weinflb.5	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
6		weinflb.6	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
7		weso	⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
8	2 7	syl	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
9		welb	⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ( ^◡ 𝑅 Or 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ^◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ^◡ 𝑅 𝑧 ) ) ) )
10	2 3 4 5 9	syl13anc	⊢ ( 𝜑 → ( ^◡ 𝑅 Or 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ^◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ^◡ 𝑅 𝑧 ) ) ) )
11	10	simprd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ^◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ^◡ 𝑅 𝑧 ) ) )
12	4	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
13	12	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ^◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ^◡ 𝑅 𝑧 ) ) ) ) → 𝑥 ∈ 𝐴 )
14		brcnvg	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ^◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) )
15	14	notbid	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑥 ^◡ 𝑅 𝑦 ↔ ¬ 𝑦 𝑅 𝑥 ) )
16	15	ralbidva	⊢ ( 𝑥 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
17	16	biimpa	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ) → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
18	17	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ) → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
19		breq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝑅 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
20		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐵 )
21		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 𝑅 𝑦 )
22	19 20 21	rspcedvdw	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 )
23	22	ex	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) )
24	23	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ^◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ^◡ 𝑅 𝑧 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) )
26	18 25	anim12dan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ^◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ^◡ 𝑅 𝑧 ) ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
27	26	anasss	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ^◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ^◡ 𝑅 𝑧 ) ) ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
28	11 13 27	reximssdv	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
29	8 28	inflb	⊢ ( 𝜑 → ( 𝐶 ∈ 𝐵 → ¬ 𝐶 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) ) )
30	6 29	mpd	⊢ ( 𝜑 → ¬ 𝐶 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) )

Metamath Proof Explorer

Theorem weinflb

Proof