prslem

	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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )

Metamath Proof Explorer

Theorem prslem

Proof