Metamath Proof Explorer

Theorem ispos

Description: The predicate "is a poset." (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 4-Nov-2013)

Ref Expression
Hypotheses ispos.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ispos.l ⊢ ≤ = ( le ‘ 𝐾 )
Assertion ispos ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 ispos.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ispos.l ⊢ ≤ = ( le ‘ 𝐾 )
3 fveq2 ⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) )
4 3 1 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 )
5 4 eqeq2d ⊢ ( 𝑝 = 𝐾 → ( 𝑏 = ( Base ‘ 𝑝 ) ↔ 𝑏 = 𝐵 ) )
6 fveq2 ⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ( le ‘ 𝐾 ) )
7 6 2 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ≤ )
8 7 eqeq2d ⊢ ( 𝑝 = 𝐾 → ( 𝑟 = ( le ‘ 𝑝 ) ↔ 𝑟 = ≤ ) )
9 5 8 3anbi12d ⊢ ( 𝑝 = 𝐾 → ( ( 𝑏 = ( Base ‘ 𝑝 ) ∧ 𝑟 = ( le ‘ 𝑝 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ↔ ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) )
10 9 2exbidv ⊢ ( 𝑝 = 𝐾 → ( ∃ 𝑏 ∃ 𝑟 ( 𝑏 = ( Base ‘ 𝑝 ) ∧ 𝑟 = ( le ‘ 𝑝 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ↔ ∃ 𝑏 ∃ 𝑟 ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) )
11 df-poset ⊢ Poset = { 𝑝 ∣ ∃ 𝑏 ∃ 𝑟 ( 𝑏 = ( Base ‘ 𝑝 ) ∧ 𝑟 = ( le ‘ 𝑝 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) }
12 10 11 elab4g ⊢ ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ V ∧ ∃ 𝑏 ∃ 𝑟 ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) )
13 1 fvexi ⊢ 𝐵 ∈ V
14 2 fvexi ⊢ ≤ ∈ V
15 raleq ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
16 15 raleqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
17 16 raleqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
18 breq ⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑥 ↔ 𝑥 ≤ 𝑥 ) )
19 breq ⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
20 breq ⊢ ( 𝑟 = ≤ → ( 𝑦 𝑟 𝑥 ↔ 𝑦 ≤ 𝑥 ) )
21 19 20 anbi12d ⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) )
22 21 imbi1d ⊢ ( 𝑟 = ≤ → ( ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ) )
23 breq ⊢ ( 𝑟 = ≤ → ( 𝑦 𝑟 𝑧 ↔ 𝑦 ≤ 𝑧 ) )
24 19 23 anbi12d ⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ) )
25 breq ⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑧 ↔ 𝑥 ≤ 𝑧 ) )
26 24 25 imbi12d ⊢ ( 𝑟 = ≤ → ( ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
27 18 22 26 3anbi123d ⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
28 27 ralbidv ⊢ ( 𝑟 = ≤ → ( ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
29 28 2ralbidv ⊢ ( 𝑟 = ≤ → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
30 13 14 17 29 ceqsex2v ⊢ ( ∃ 𝑏 ∃ 𝑟 ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
31 30 anbi2i ⊢ ( ( 𝐾 ∈ V ∧ ∃ 𝑏 ∃ 𝑟 ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
32 12 31 bitri ⊢ ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )