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 ⊢ φ → K ∈ V
pospropd.lv ⊢ φ → L ∈ W
pospropd.kb ⊢ φ → B = Base K
pospropd.lb ⊢ φ → B = Base L
pospropd.xy ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ≤ K y ↔ x ≤ L y
Assertion pospropd ⊢ φ → K ∈ Poset ↔ L ∈ Poset

Proof

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