Theorem isposd 18286

Description: Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by AV, 26-Apr-2024.)

Hypotheses

Ref	Expression
isposd.k	⊢ (𝜑 → 𝐾 ∈ 𝑉)
isposd.b	⊢ (𝜑 → 𝐵 = (Base‘𝐾))
isposd.l	⊢ (𝜑 → ≤ = (le‘𝐾))
isposd.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥)
isposd.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))
isposd.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))

Assertion

Ref	Expression
isposd	⊢ (𝜑 → 𝐾 ∈ Poset)

Distinct variable groups:   𝑥,𝑦,𝑧,𝐵   𝑥,𝐾,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧

Allowed substitution hints:   ≤ (𝑥,𝑦,𝑧)   𝑉(𝑥,𝑦,𝑧)

Proof of Theorem isposd

Step	Hyp	Ref	Expression
1		isposd.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ 𝑉)
2	1	elexd 3456	. . 3 ⊢ (𝜑 → 𝐾 ∈ V)
3		isposd.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥)
4	3	adantrr 723	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ≤ 𝑥)
5	4	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑥 ≤ 𝑥)
6		isposd.2	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))
7	6	3expb 1126	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))
8	7	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))
9		isposd.3	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))
10	9	3exp2 1361	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))))
11	10	imp42 427	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))
12	5, 8, 11	3jca 1134	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
13	12	ralrimiva 3132	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
14	13	ralrimivva 3183	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
15		isposd.b	. . . . 5 ⊢ (𝜑 → 𝐵 = (Base‘𝐾))
16		isposd.l	. . . . . . . . 9 ⊢ (𝜑 → ≤ = (le‘𝐾))
17	16	breqd 5090	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ≤ 𝑥 ↔ 𝑥(le‘𝐾)𝑥))
18	16	breqd 5090	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ≤ 𝑦 ↔ 𝑥(le‘𝐾)𝑦))
19	16	breqd 5090	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ≤ 𝑥 ↔ 𝑦(le‘𝐾)𝑥))
20	18, 19	anbi12d 638	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ (𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥)))
21	20	imbi1d 342	. . . . . . . 8 ⊢ (𝜑 → (((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ↔ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦)))
22	16	breqd 5090	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ≤ 𝑧 ↔ 𝑦(le‘𝐾)𝑧))
23	18, 22	anbi12d 638	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) ↔ (𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧)))
24	16	breqd 5090	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ≤ 𝑧 ↔ 𝑥(le‘𝐾)𝑧))
25	23, 24	imbi12d 345	. . . . . . . 8 ⊢ (𝜑 → (((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧) ↔ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))
26	17, 21, 25	3anbi123d 1444	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
27	15, 26	raleqbidv 3314	. . . . . 6 ⊢ (𝜑 → (∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
28	15, 27	raleqbidv 3314	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
29	15, 28	raleqbidv 3314	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
30	29	anbi2d 636	. . 3 ⊢ (𝜑 → ((𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))) ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))))
31	2, 14, 30	mpbi2and 718	. 2 ⊢ (𝜑 → (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
32		eqid 2740	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
33		eqid 2740	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
34	32, 33	ispos 18278	. 2 ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
35	31, 34	sylibr 235	1 ⊢ (𝜑 → 𝐾 ∈ Poset)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3054  Vcvv 3432   class class class wbr 5079  ‘cfv 6492  Basecbs 17177  lecple 17225  Posetcpo 18271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-poset 18277

This theorem is referenced by:  odupos  18290  pospo  18307  ipopos  18500  zntoslem  21538  resipos  49472