Metamath Proof Explorer

Theorem postcposALT

Description: Alternate proof for postcpos . (Contributed by Zhi Wang, 25-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses postc.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
postc.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
Assertion postcposALT ( 𝜑 → ( 𝐾 ∈ Poset ↔ 𝐶 ∈ Poset ) )

Proof

Step Hyp Ref Expression
1 postc.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2 postc.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
3 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
4 1 2 3 prstcbas ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐶 ) )
5 eqidd ⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) )
6 1 2 5 prstcle ⊢ ( 𝜑 → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐶 ) 𝑦 ) )
7 1 2 5 prstcle ⊢ ( 𝜑 → ( 𝑦 ( le ‘ 𝐾 ) 𝑥 ↔ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) )
8 6 7 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) ↔ ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) ) )
9 8 imbi1d ⊢ ( 𝜑 → ( ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
10 4 9 raleqbidvv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
11 4 10 raleqbidvv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
14 12 13 ispos2 ⊢ ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
15 14 baib ⊢ ( 𝐾 ∈ Proset → ( 𝐾 ∈ Poset ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
16 2 15 syl ⊢ ( 𝜑 → ( 𝐾 ∈ Poset ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
17 1 2 prstcprs ⊢ ( 𝜑 → 𝐶 ∈ Proset )
18 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
19 eqid ⊢ ( le ‘ 𝐶 ) = ( le ‘ 𝐶 )
20 18 19 ispos2 ⊢ ( 𝐶 ∈ Poset ↔ ( 𝐶 ∈ Proset ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
21 20 baib ⊢ ( 𝐶 ∈ Proset → ( 𝐶 ∈ Poset ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
22 17 21 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Poset ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
23 11 16 22 3bitr4d ⊢ ( 𝜑 → ( 𝐾 ∈ Poset ↔ 𝐶 ∈ Poset ) )