Theorem isposd 18368

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 3504	. . 3 ⊢ (𝜑 → 𝐾 ∈ V)
3		isposd.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥)
4	3	adantrr 717	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ≤ 𝑥)
5	4	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑥 ≤ 𝑥)
6		isposd.2	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))
7	6	3expb 1121	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))
8	7	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))
9		isposd.3	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))
10	9	3exp2 1355	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))))
11	10	imp42 426	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))
12	5, 8, 11	3jca 1129	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
13	12	ralrimiva 3146	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
14	13	ralrimivva 3202	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
15		isposd.b	. . . . 5 ⊢ (𝜑 → 𝐵 = (Base‘𝐾))
16		isposd.l	. . . . . . . . 9 ⊢ (𝜑 → ≤ = (le‘𝐾))
17	16	breqd 5154	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ≤ 𝑥 ↔ 𝑥(le‘𝐾)𝑥))
18	16	breqd 5154	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ≤ 𝑦 ↔ 𝑥(le‘𝐾)𝑦))
19	16	breqd 5154	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ≤ 𝑥 ↔ 𝑦(le‘𝐾)𝑥))
20	18, 19	anbi12d 632	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ (𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥)))
21	20	imbi1d 341	. . . . . . . 8 ⊢ (𝜑 → (((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ↔ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦)))
22	16	breqd 5154	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ≤ 𝑧 ↔ 𝑦(le‘𝐾)𝑧))
23	18, 22	anbi12d 632	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) ↔ (𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧)))
24	16	breqd 5154	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ≤ 𝑧 ↔ 𝑥(le‘𝐾)𝑧))
25	23, 24	imbi12d 344	. . . . . . . 8 ⊢ (𝜑 → (((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧) ↔ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))
26	17, 21, 25	3anbi123d 1438	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
27	15, 26	raleqbidv 3346	. . . . . 6 ⊢ (𝜑 → (∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
28	15, 27	raleqbidv 3346	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
29	15, 28	raleqbidv 3346	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
30	29	anbi2d 630	. . 3 ⊢ (𝜑 → ((𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))) ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))))
31	2, 14, 30	mpbi2and 712	. 2 ⊢ (𝜑 → (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
32		eqid 2737	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
33		eqid 2737	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
34	32, 33	ispos 18360	. 2 ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))
35	31, 34	sylibr 234	1 ⊢ (𝜑 → 𝐾 ∈ Poset)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480   class class class wbr 5143  ‘cfv 6561  Basecbs 17247  lecple 17304  Posetcpo 18353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-poset 18359

This theorem is referenced by:  odupos  18373  pospo  18390  ipopos  18581  zntoslem  21575