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

Metamath Proof Explorer

Theorem prslem

Description: Lemma for prsref and prstr . (Contributed by Mario Carneiro, 1-Feb-2015)

Ref Expression
Hypotheses isprs.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
isprs.l ⊢ ≤ = ( le ‘ 𝐾 )
Assertion prslem ( ( 𝐾 ∈ Proset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 isprs.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isprs.l ⊢ ≤ = ( le ‘ 𝐾 )
3 1 2 isprs ⊢ ( 𝐾 ∈ Proset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
4 3 simprbi ⊢ ( 𝐾 ∈ Proset → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
5 breq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ≤ 𝑥 ↔ 𝑋 ≤ 𝑋 ) )
6 5 anidms ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑥 ↔ 𝑋 ≤ 𝑋 ) )
7 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦 ) )
8 7 anbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ) )
9 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑧 ↔ 𝑋 ≤ 𝑧 ) )
10 8 9 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ↔ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) )
11 6 10 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) ) )
12 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌 ) )
13 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ≤ 𝑧 ↔ 𝑌 ≤ 𝑧 ) )
14 12 13 anbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) ) )
15 14 imbi1d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ↔ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) )
16 15 anbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) ↔ ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) ) )
17 breq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑌 ≤ 𝑧 ↔ 𝑌 ≤ 𝑍 ) )
18 17 anbi2d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) )
19 breq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑋 ≤ 𝑧 ↔ 𝑋 ≤ 𝑍 ) )
20 18 19 imbi12d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ↔ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )
21 20 anbi2d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) ↔ ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) ) )
22 11 16 21 rspc3v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) ) )
23 4 22 mpan9 ⊢ ( ( 𝐾 ∈ Proset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )