Metamath Proof Explorer

Theorem ordtbaslem

Description: Lemma for ordtbas . In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 ⊢X=dom⁡R
ordtval.2 ⊢A=ran⁡x∈X⟼y∈X|¬yRx
Assertion ordtbaslem ⊢R∈TosetRel→fi⁡A=A

Proof

Step Hyp Ref Expression
1 ordtval.1 ⊢X=dom⁡R
2 ordtval.2 ⊢A=ran⁡x∈X⟼y∈X|¬yRx
3 3anrot ⊢y∈X∧a∈X∧b∈X↔a∈X∧b∈X∧y∈X
4 1 tsrlemax ⊢R∈TosetRel∧y∈X∧a∈X∧b∈X→yRifaRbba↔yRa∨yRb
5 3 4 sylan2br ⊢R∈TosetRel∧a∈X∧b∈X∧y∈X→yRifaRbba↔yRa∨yRb
6 5 3exp2 ⊢R∈TosetRel→a∈X→b∈X→y∈X→yRifaRbba↔yRa∨yRb
7 6 imp42 ⊢R∈TosetRel∧a∈X∧b∈X∧y∈X→yRifaRbba↔yRa∨yRb
8 7 notbid ⊢R∈TosetRel∧a∈X∧b∈X∧y∈X→¬yRifaRbba↔¬yRa∨yRb
9 ioran ⊢¬yRa∨yRb↔¬yRa∧¬yRb
10 8 9 bitrdi ⊢R∈TosetRel∧a∈X∧b∈X∧y∈X→¬yRifaRbba↔¬yRa∧¬yRb
11 10 rabbidva ⊢R∈TosetRel∧a∈X∧b∈X→y∈X|¬yRifaRbba=y∈X|¬yRa∧¬yRb
12 ifcl ⊢b∈X∧a∈X→ifaRbba∈X
13 12 ancoms ⊢a∈X∧b∈X→ifaRbba∈X
14 dmexg ⊢R∈TosetRel→dom⁡R∈V
15 1 14 eqeltrid ⊢R∈TosetRel→X∈V
16 15 adantr ⊢R∈TosetRel∧a∈X∧b∈X→X∈V
17 rabexg ⊢X∈V→y∈X|¬yRa∧¬yRb∈V
18 16 17 syl ⊢R∈TosetRel∧a∈X∧b∈X→y∈X|¬yRa∧¬yRb∈V
19 11 18 eqeltrd ⊢R∈TosetRel∧a∈X∧b∈X→y∈X|¬yRifaRbba∈V
20 eqid ⊢x∈X⟼y∈X|¬yRx=x∈X⟼y∈X|¬yRx
21 breq2 ⊢x=ifaRbba→yRx↔yRifaRbba
22 21 notbid ⊢x=ifaRbba→¬yRx↔¬yRifaRbba
23 22 rabbidv ⊢x=ifaRbba→y∈X|¬yRx=y∈X|¬yRifaRbba
24 20 23 elrnmpt1s ⊢ifaRbba∈X∧y∈X|¬yRifaRbba∈V→y∈X|¬yRifaRbba∈ran⁡x∈X⟼y∈X|¬yRx
25 24 2 eleqtrrdi ⊢ifaRbba∈X∧y∈X|¬yRifaRbba∈V→y∈X|¬yRifaRbba∈A
26 13 19 25 syl2an2 ⊢R∈TosetRel∧a∈X∧b∈X→y∈X|¬yRifaRbba∈A
27 11 26 eqeltrrd ⊢R∈TosetRel∧a∈X∧b∈X→y∈X|¬yRa∧¬yRb∈A
28 27 ralrimivva ⊢R∈TosetRel→∀a∈X∀b∈Xy∈X|¬yRa∧¬yRb∈A
29 rabexg ⊢X∈V→y∈X|¬yRa∈V
30 15 29 syl ⊢R∈TosetRel→y∈X|¬yRa∈V
31 30 ralrimivw ⊢R∈TosetRel→∀a∈Xy∈X|¬yRa∈V
32 breq2 ⊢x=a→yRx↔yRa
33 32 notbid ⊢x=a→¬yRx↔¬yRa
34 33 rabbidv ⊢x=a→y∈X|¬yRx=y∈X|¬yRa
35 34 cbvmptv ⊢x∈X⟼y∈X|¬yRx=a∈X⟼y∈X|¬yRa
36 ineq1 ⊢z=y∈X|¬yRa→z∩y∈X|¬yRb=y∈X|¬yRa∩y∈X|¬yRb
37 inrab ⊢y∈X|¬yRa∩y∈X|¬yRb=y∈X|¬yRa∧¬yRb
38 36 37 eqtrdi ⊢z=y∈X|¬yRa→z∩y∈X|¬yRb=y∈X|¬yRa∧¬yRb
39 38 eleq1d ⊢z=y∈X|¬yRa→z∩y∈X|¬yRb∈A↔y∈X|¬yRa∧¬yRb∈A
40 39 ralbidv ⊢z=y∈X|¬yRa→∀b∈Xz∩y∈X|¬yRb∈A↔∀b∈Xy∈X|¬yRa∧¬yRb∈A
41 35 40 ralrnmptw ⊢∀a∈Xy∈X|¬yRa∈V→∀z∈ran⁡x∈X⟼y∈X|¬yRx∀b∈Xz∩y∈X|¬yRb∈A↔∀a∈X∀b∈Xy∈X|¬yRa∧¬yRb∈A
42 31 41 syl ⊢R∈TosetRel→∀z∈ran⁡x∈X⟼y∈X|¬yRx∀b∈Xz∩y∈X|¬yRb∈A↔∀a∈X∀b∈Xy∈X|¬yRa∧¬yRb∈A
43 28 42 mpbird ⊢R∈TosetRel→∀z∈ran⁡x∈X⟼y∈X|¬yRx∀b∈Xz∩y∈X|¬yRb∈A
44 rabexg ⊢X∈V→y∈X|¬yRb∈V
45 15 44 syl ⊢R∈TosetRel→y∈X|¬yRb∈V
46 45 ralrimivw ⊢R∈TosetRel→∀b∈Xy∈X|¬yRb∈V
47 breq2 ⊢x=b→yRx↔yRb
48 47 notbid ⊢x=b→¬yRx↔¬yRb
49 48 rabbidv ⊢x=b→y∈X|¬yRx=y∈X|¬yRb
50 49 cbvmptv ⊢x∈X⟼y∈X|¬yRx=b∈X⟼y∈X|¬yRb
51 ineq2 ⊢w=y∈X|¬yRb→z∩w=z∩y∈X|¬yRb
52 51 eleq1d ⊢w=y∈X|¬yRb→z∩w∈A↔z∩y∈X|¬yRb∈A
53 50 52 ralrnmptw ⊢∀b∈Xy∈X|¬yRb∈V→∀w∈ran⁡x∈X⟼y∈X|¬yRxz∩w∈A↔∀b∈Xz∩y∈X|¬yRb∈A
54 46 53 syl ⊢R∈TosetRel→∀w∈ran⁡x∈X⟼y∈X|¬yRxz∩w∈A↔∀b∈Xz∩y∈X|¬yRb∈A
55 54 ralbidv ⊢R∈TosetRel→∀z∈ran⁡x∈X⟼y∈X|¬yRx∀w∈ran⁡x∈X⟼y∈X|¬yRxz∩w∈A↔∀z∈ran⁡x∈X⟼y∈X|¬yRx∀b∈Xz∩y∈X|¬yRb∈A
56 43 55 mpbird ⊢R∈TosetRel→∀z∈ran⁡x∈X⟼y∈X|¬yRx∀w∈ran⁡x∈X⟼y∈X|¬yRxz∩w∈A
57 2 raleqi ⊢∀w∈Az∩w∈A↔∀w∈ran⁡x∈X⟼y∈X|¬yRxz∩w∈A
58 2 57 raleqbii ⊢∀z∈A∀w∈Az∩w∈A↔∀z∈ran⁡x∈X⟼y∈X|¬yRx∀w∈ran⁡x∈X⟼y∈X|¬yRxz∩w∈A
59 56 58 sylibr ⊢R∈TosetRel→∀z∈A∀w∈Az∩w∈A
60 15 pwexd ⊢R∈TosetRel→𝒫X∈V
61 ssrab2 ⊢y∈X|¬yRx⊆X
62 15 adantr ⊢R∈TosetRel∧x∈X→X∈V
63 elpw2g ⊢X∈V→y∈X|¬yRx∈𝒫X↔y∈X|¬yRx⊆X
64 62 63 syl ⊢R∈TosetRel∧x∈X→y∈X|¬yRx∈𝒫X↔y∈X|¬yRx⊆X
65 61 64 mpbiri ⊢R∈TosetRel∧x∈X→y∈X|¬yRx∈𝒫X
66 65 fmpttd ⊢R∈TosetRel→x∈X⟼y∈X|¬yRx:X⟶𝒫X
67 66 frnd ⊢R∈TosetRel→ran⁡x∈X⟼y∈X|¬yRx⊆𝒫X
68 2 67 eqsstrid ⊢R∈TosetRel→A⊆𝒫X
69 60 68 ssexd ⊢R∈TosetRel→A∈V
70 inficl ⊢A∈V→∀z∈A∀w∈Az∩w∈A↔fi⁡A=A
71 69 70 syl ⊢R∈TosetRel→∀z∈A∀w∈Az∩w∈A↔fi⁡A=A
72 59 71 mpbid ⊢R∈TosetRel→fi⁡A=A