Theorem glb0 17849

Description: The greatest lower bound of the empty set is the unit element.

Hypotheses

Ref	Expression
glb0.g	|- G = (glb` K)
glb0.u	|- U = (1.` K)

Assertion

Ref	Expression
glb0	|- (K e. OP -> (G` (/)) = U)

Proof of Theorem glb0

Step	Hyp	Ref	Expression
1		0ss 3139	. . 3 |- (/) C_ (Base` K)
2		eqid 2170	. . . 4 |- (Base` K) = (Base` K)
3		eqid 2170	. . . 4 |- (le` K) = (le` K)
4		glb0.g	. . . 4 |- G = (glb` K)
5	2, 3, 4	glbval 9728	. . 3 |- ((K e. OP /\ (/) C_ (Base` K)) -> (G` (/)) = (iota_x e. (Base` K)(A.y e. (/) x(le` K)y /\ A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x))))
6	1, 5	mpan2 775	. 2 |- (K e. OP -> (G` (/)) = (iota_x e. (Base` K)(A.y e. (/) x(le` K)y /\ A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x))))
7		glb0.u	. . . 4 |- U = (1.` K)
8	2, 7	op1cl 17842	. . 3 |- (K e. OP -> U e. (Base` K))
9		ral0 3205	. . . . . . . 8 |- A.y e. (/) z(le` K)y
10	9	a1bi 400	. . . . . . 7 |- (z(le` K)x <-> (A.y e. (/) z(le` K)y -> z(le` K)x))
11	10	ralbii 2407	. . . . . 6 |- (A.z e. (Base` K)z(le` K)x <-> A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x))
12		ral0 3205	. . . . . . 7 |- A.y e. (/) x(le` K)y
13	12	biantrur 1000	. . . . . 6 |- (A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x) <-> (A.y e. (/) x(le` K)y /\ A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x)))
14	11, 13	bitri 306	. . . . 5 |- (A.z e. (Base` K)z(le` K)x <-> (A.y e. (/) x(le` K)y /\ A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x)))
15		breq1 3542	. . . . . . . . 9 |- (z = U -> (z(le` K)x <-> U(le` K)x))
16	15	rcla4v 2647	. . . . . . . 8 |- (U e. (Base` K) -> (A.z e. (Base` K)z(le` K)x -> U(le` K)x))
17	16	3ad2ant2 1170	. . . . . . 7 |- ((K e. OP /\ U e. (Base` K) /\ x e. (Base` K)) -> (A.z e. (Base` K)z(le` K)x -> U(le` K)x))
18	2, 3, 7	op1le 17848	. . . . . . . 8 |- ((K e. OP /\ x e. (Base` K)) -> (U(le` K)x <-> x = U))
19	18	3adant2 1167	. . . . . . 7 |- ((K e. OP /\ U e. (Base` K) /\ x e. (Base` K)) -> (U(le` K)x <-> x = U))
20	17, 19	sylibd 266	. . . . . 6 |- ((K e. OP /\ U e. (Base` K) /\ x e. (Base` K)) -> (A.z e. (Base` K)z(le` K)x -> x = U))
21	2, 3, 7	ople1 17847	. . . . . . . . 9 |- ((K e. OP /\ z e. (Base` K)) -> z(le` K)U)
22	21	3ad2antl1 1316	. . . . . . . 8 |- (((K e. OP /\ U e. (Base` K) /\ x e. (Base` K)) /\ z e. (Base` K)) -> z(le` K)U)
23		breq2 3543	. . . . . . . 8 |- (x = U -> (z(le` K)x <-> z(le` K)U))
24	22, 23	syl5ibrcom 279	. . . . . . 7 |- (((K e. OP /\ U e. (Base` K) /\ x e. (Base` K)) /\ z e. (Base` K)) -> (x = U -> z(le` K)x))
25	24	r19.21adva 2462	. . . . . 6 |- ((K e. OP /\ U e. (Base` K) /\ x e. (Base` K)) -> (x = U -> A.z e. (Base` K)z(le` K)x))
26	20, 25	impbid 250	. . . . 5 |- ((K e. OP /\ U e. (Base` K) /\ x e. (Base` K)) -> (A.z e. (Base` K)z(le` K)x <-> x = U))
27	14, 26	syl5bbr 320	. . . 4 |- ((K e. OP /\ U e. (Base` K) /\ x e. (Base` K)) -> ((A.y e. (/) x(le` K)y /\ A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x)) <-> x = U))
28	27	riota5 5799	. . 3 |- ((K e. OP /\ U e. (Base` K)) -> (iota_x e. (Base` K)(A.y e. (/) x(le` K)y /\ A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x))) = U)
29	8, 28	mpdan 769	. 2 |- (K e. OP -> (iota_x e. (Base` K)(A.y e. (/) x(le` K)y /\ A.z e. (Base` K)(A.y e. (/) z(le` K)y -> z(le` K)x))) = U)
30	6, 29	eqtrd 2202	1 |- (K e. OP -> (G` (/)) = U)

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617  A.wral 2385   C_ wss 2859  (/)c0 3114   class class class wbr 3539  ` cfv 4163  iota_crio 5768  Basecbs 9579  lecple 9687  glbcglb 9691  1.cp1 9750  OPcops 17828

This theorem is referenced by:  pmapglb2 18475  pmapglb2x 18476

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-id 3779  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-mpt 5138  df-iota 5259  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-poset 9697  df-lub 9718  df-glb 9719  df-p1 9753  df-oposet 17833

Copyright terms: Public domain