Theorem ordtprsuni 34112

Description: Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.)

Hypotheses

Ref	Expression
ordtNEW.b	⊢ 𝐵 = (Base‘𝐾)
ordtNEW.l	⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
ordtposval.e	⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
ordtposval.f	⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})

Assertion

Ref	Expression
ordtprsuni	⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹)))

Distinct variable groups:   𝑥,𝑦, ≤   𝑥,𝐵,𝑦   𝑥,𝐾,𝑦

Allowed substitution hints:   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem ordtprsuni

Step	Hyp	Ref	Expression
1		ordtNEW.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
2		ordtNEW.l	. . . . . 6 ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
3	1, 2	prsdm 34107	. . . . 5 ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵)
4	3	sneqd 4568	. . . 4 ⊢ (𝐾 ∈ Proset → {dom ≤ } = {𝐵})
5		biidd 263	. . . . . . . 8 ⊢ (𝐾 ∈ Proset → (¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ≤ 𝑥))
6	3, 5	rabeqbidv 3409	. . . . . . 7 ⊢ (𝐾 ∈ Proset → {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
7	3, 6	mpteq12dv 5160	. . . . . 6 ⊢ (𝐾 ∈ Proset → (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
8	7	rneqd 5881	. . . . 5 ⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
9		biidd 263	. . . . . . . 8 ⊢ (𝐾 ∈ Proset → (¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑥 ≤ 𝑦))
10	3, 9	rabeqbidv 3409	. . . . . . 7 ⊢ (𝐾 ∈ Proset → {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
11	3, 10	mpteq12dv 5160	. . . . . 6 ⊢ (𝐾 ∈ Proset → (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
12	11	rneqd 5881	. . . . 5 ⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
13	8, 12	uneq12d 4100	. . . 4 ⊢ (𝐾 ∈ Proset → (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})) = (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))
14	4, 13	uneq12d 4100	. . 3 ⊢ (𝐾 ∈ Proset → ({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))) = ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
15	14	unieqd 4852	. 2 ⊢ (𝐾 ∈ Proset → ∪ ({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))) = ∪ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
16		fvex 6841	. . . . . 6 ⊢ (le‘𝐾) ∈ V
17	16	inex1 5246	. . . . 5 ⊢ ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
18	2, 17	eqeltri 2835	. . . 4 ⊢ ≤ ∈ V
19		eqid 2739	. . . . 5 ⊢ dom ≤ = dom ≤
20		eqid 2739	. . . . 5 ⊢ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥})
21		eqid 2739	. . . . 5 ⊢ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})
22	19, 20, 21	ordtuni 23174	. . . 4 ⊢ ( ≤ ∈ V → dom ≤ = ∪ ({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))))
23	18, 22	ax-mp 5	. . 3 ⊢ dom ≤ = ∪ ({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})))
24	3, 23	eqtr3di 2789	. 2 ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))))
25		ordtposval.e	. . . . . 6 ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
26		ordtposval.f	. . . . . 6 ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
27	25, 26	uneq12i 4097	. . . . 5 ⊢ (𝐸 ∪ 𝐹) = (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
28	27	a1i 11	. . . 4 ⊢ (𝐾 ∈ Proset → (𝐸 ∪ 𝐹) = (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))
29	28	uneq2d 4099	. . 3 ⊢ (𝐾 ∈ Proset → ({𝐵} ∪ (𝐸 ∪ 𝐹)) = ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
30	29	unieqd 4852	. 2 ⊢ (𝐾 ∈ Proset → ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹)) = ∪ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
31	15, 24, 30	3eqtr4d 2784	1 ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹)))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119  {crab 3391  Vcvv 3431   ∪ cun 3881   ∩ cin 3882  {csn 4556  ∪ cuni 4839   class class class wbr 5073   ↦ cmpt 5154   × cxp 5617  dom cdm 5619  ran crn 5620  ‘cfv 6486  Basecbs 17171  lecple 17219   Proset cproset 18250

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-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pr 5363  ax-un 7679

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-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-proset 18252

This theorem is referenced by:  ordtrest2NEW  34116