This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem catprslem

Description: Lemma for catprs . (Contributed by Zhi Wang, 18-Sep-2024)

Ref Expression
Hypotheses catprs.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) )
catprslem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
catprslem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion catprslem ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 catprs.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) )
2 catprslem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
3 catprslem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦 ) )
5 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑦 ) )
6 5 neeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 𝐻 𝑦 ) ≠ ∅ ↔ ( 𝑧 𝐻 𝑦 ) ≠ ∅ ) )
7 4 6 bibi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) ↔ ( 𝑧 ≤ 𝑦 ↔ ( 𝑧 𝐻 𝑦 ) ≠ ∅ ) ) )
8 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 ≤ 𝑦 ↔ 𝑧 ≤ 𝑤 ) )
9 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑤 ) )
10 9 neeq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 𝐻 𝑦 ) ≠ ∅ ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
11 8 10 bibi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 ≤ 𝑦 ↔ ( 𝑧 𝐻 𝑦 ) ≠ ∅ ) ↔ ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) ) )
12 7 11 cbvral2vw ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
13 1 12 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
14 breq12 ⊢ ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) → ( 𝑧 ≤ 𝑤 ↔ 𝑋 ≤ 𝑌 ) )
15 oveq12 ⊢ ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) → ( 𝑧 𝐻 𝑤 ) = ( 𝑋 𝐻 𝑌 ) )
16 15 neeq1d ⊢ ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) → ( ( 𝑧 𝐻 𝑤 ) ≠ ∅ ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) )
17 14 16 bibi12d ⊢ ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) → ( ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) ↔ ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) ) )
18 17 rspc2gv ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) ) )
19 2 3 18 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) ) )
20 13 19 mpd ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) )