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

Metamath Proof Explorer

Theorem pospropd

Description: Posethood is determined only by structure components and only by the value of the relation within the base set. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypotheses pospropd.kv ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
pospropd.lv ⊢ ( 𝜑 → 𝐿 ∈ 𝑊 )
pospropd.kb ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
pospropd.lb ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
pospropd.xy ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) )
Assertion pospropd ( 𝜑 → ( 𝐾 ∈ Poset ↔ 𝐿 ∈ Poset ) )

Proof

Step Hyp Ref Expression
1 pospropd.kv ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
2 pospropd.lv ⊢ ( 𝜑 → 𝐿 ∈ 𝑊 )
3 pospropd.kb ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
4 pospropd.lb ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
5 pospropd.xy ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) )
6 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) )
7 simp1 ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
8 7 7 jca ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) )
9 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐾 ) 𝑦 ) )
10 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ( le ‘ 𝐿 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑦 ) )
11 9 10 bibi12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ↔ ( 𝑎 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑦 ) ) )
12 breq2 ⊢ ( 𝑦 = 𝑎 → ( 𝑎 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐾 ) 𝑎 ) )
13 breq2 ⊢ ( 𝑦 = 𝑎 → ( 𝑎 ( le ‘ 𝐿 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑎 ) )
14 12 13 bibi12d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑦 ) ↔ ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑎 ) ) )
15 11 14 rspc2va ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑎 ) )
16 8 15 sylan ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑎 ) )
17 breq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐾 ) 𝑏 ) )
18 breq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 ( le ‘ 𝐿 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑏 ) )
19 17 18 bibi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑦 ) ↔ ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑏 ) ) )
20 11 19 rspc2va ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑏 ) )
21 20 3adantl3 ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑏 ) )
22 3simpb ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) )
23 22 3comr ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) )
24 breq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐾 ) 𝑦 ) )
25 breq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 ( le ‘ 𝐿 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑦 ) )
26 24 25 bibi12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ↔ ( 𝑏 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑦 ) ) )
27 breq2 ⊢ ( 𝑦 = 𝑎 → ( 𝑏 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) )
28 breq2 ⊢ ( 𝑦 = 𝑎 → ( 𝑏 ( le ‘ 𝐿 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) )
29 27 28 bibi12d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑏 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑦 ) ↔ ( 𝑏 ( le ‘ 𝐾 ) 𝑎 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) ) )
30 26 29 rspc2va ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑏 ( le ‘ 𝐾 ) 𝑎 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) )
31 23 30 sylan ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑏 ( le ‘ 𝐾 ) 𝑎 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) )
32 21 31 anbi12d ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) ↔ ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) ) )
33 32 imbi1d ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ↔ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ) )
34 breq2 ⊢ ( 𝑦 = 𝑐 → ( 𝑏 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) )
35 breq2 ⊢ ( 𝑦 = 𝑐 → ( 𝑏 ( le ‘ 𝐿 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) )
36 34 35 bibi12d ⊢ ( 𝑦 = 𝑐 → ( ( 𝑏 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑦 ) ↔ ( 𝑏 ( le ‘ 𝐾 ) 𝑐 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) ) )
37 26 36 rspc2va ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑏 ( le ‘ 𝐾 ) 𝑐 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) )
38 37 3adantl1 ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑏 ( le ‘ 𝐾 ) 𝑐 ↔ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) )
39 21 38 anbi12d ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) ↔ ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) ) )
40 3simpb ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑎 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) )
41 breq2 ⊢ ( 𝑦 = 𝑐 → ( 𝑎 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐾 ) 𝑐 ) )
42 breq2 ⊢ ( 𝑦 = 𝑐 → ( 𝑎 ( le ‘ 𝐿 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑐 ) )
43 41 42 bibi12d ⊢ ( 𝑦 = 𝑐 → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑦 ) ↔ ( 𝑎 ( le ‘ 𝐾 ) 𝑐 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) )
44 11 43 rspc2va ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑎 ( le ‘ 𝐾 ) 𝑐 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑐 ) )
45 40 44 sylan ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( 𝑎 ( le ‘ 𝐾 ) 𝑐 ↔ 𝑎 ( le ‘ 𝐿 ) 𝑐 ) )
46 39 45 imbi12d ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ↔ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) )
47 16 33 46 3anbi123d ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐿 ) 𝑦 ) ) → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
48 6 47 sylan2 ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ 𝜑 ) → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
49 48 ancoms ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
50 49 3exp2 ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 → ( 𝑏 ∈ 𝐵 → ( 𝑐 ∈ 𝐵 → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) ) ) ) )
51 50 imp42 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
52 51 ralbidva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
53 52 2ralbidva ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
54 raleq ⊢ ( 𝐵 = ( Base ‘ 𝐾 ) → ( ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) )
55 54 raleqbi1dv ⊢ ( 𝐵 = ( Base ‘ 𝐾 ) → ( ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) )
56 55 raleqbi1dv ⊢ ( 𝐵 = ( Base ‘ 𝐾 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) )
57 3 56 syl ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) )
58 raleq ⊢ ( 𝐵 = ( Base ‘ 𝐿 ) → ( ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ↔ ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
59 58 raleqbi1dv ⊢ ( 𝐵 = ( Base ‘ 𝐿 ) → ( ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
60 59 raleqbi1dv ⊢ ( 𝐵 = ( Base ‘ 𝐿 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
61 4 60 syl ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
62 53 57 61 3bitr3d ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
63 1 elexd ⊢ ( 𝜑 → 𝐾 ∈ V )
64 63 biantrurd ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ( 𝐾 ∈ V ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) ) )
65 2 elexd ⊢ ( 𝜑 → 𝐿 ∈ V )
66 65 biantrurd ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ↔ ( 𝐿 ∈ V ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) ) )
67 62 64 66 3bitr3d ⊢ ( 𝜑 → ( ( 𝐾 ∈ V ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) ↔ ( 𝐿 ∈ V ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) ) )
68 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
69 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
70 68 69 ispos ⊢ ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ∀ 𝑐 ∈ ( Base ‘ 𝐾 ) ( 𝑎 ( le ‘ 𝐾 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐾 ) 𝑐 ) → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) )
71 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
72 eqid ⊢ ( le ‘ 𝐿 ) = ( le ‘ 𝐿 )
73 71 72 ispos ⊢ ( 𝐿 ∈ Poset ↔ ( 𝐿 ∈ V ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ∀ 𝑐 ∈ ( Base ‘ 𝐿 ) ( 𝑎 ( le ‘ 𝐿 ) 𝑎 ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ( le ‘ 𝐿 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐿 ) 𝑐 ) → 𝑎 ( le ‘ 𝐿 ) 𝑐 ) ) ) )
74 67 70 73 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ Poset ↔ 𝐿 ∈ Poset ) )