Metamath Proof Explorer

Theorem posi

Description: Lemma for poset properties. (Contributed by NM, 11-Sep-2011)

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

Proof

Step Hyp Ref Expression
1 posi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 posi.l ⊢ ≤ = ( le ‘ 𝐾 )
3 1 2 ispos ⊢ ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
4 3 simprbi ⊢ ( 𝐾 ∈ Poset → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
5 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑥 ↔ 𝑋 ≤ 𝑥 ) )
6 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑋 ≤ 𝑥 ↔ 𝑋 ≤ 𝑋 ) )
7 5 6 bitrd ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑥 ↔ 𝑋 ≤ 𝑋 ) )
8 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦 ) )
9 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑋 ) )
10 8 9 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ↔ ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑋 ) ) )
11 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑦 ) )
12 10 11 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑋 ) → 𝑋 = 𝑦 ) ) )
13 8 anbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ) )
14 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑧 ↔ 𝑋 ≤ 𝑧 ) )
15 13 14 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ↔ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) )
16 7 12 15 3anbi123d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑋 ) → 𝑋 = 𝑦 ) ∧ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) ) )
17 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌 ) )
18 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ≤ 𝑋 ↔ 𝑌 ≤ 𝑋 ) )
19 17 18 anbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑋 ) ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ) )
20 eqeq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑌 ) )
21 19 20 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑋 ) → 𝑋 = 𝑦 ) ↔ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ) )
22 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ≤ 𝑧 ↔ 𝑌 ≤ 𝑧 ) )
23 17 22 anbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) ) )
24 23 imbi1d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ↔ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) )
25 21 24 3anbi23d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑋 ) → 𝑋 = 𝑦 ) ∧ ( ( 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) ↔ ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) ) )
26 breq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑌 ≤ 𝑧 ↔ 𝑌 ≤ 𝑍 ) )
27 26 anbi2d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) )
28 breq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑋 ≤ 𝑧 ↔ 𝑋 ≤ 𝑍 ) )
29 27 28 imbi12d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ↔ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )
30 29 3anbi3d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑧 ) → 𝑋 ≤ 𝑧 ) ) ↔ ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) ) )
31 16 25 30 rspc3v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) ) )
32 4 31 mpan9 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )