Metamath Proof Explorer


Theorem opnvonmbllem2

Description: An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses opnvonmbllem2.x φ X Fin
opnvonmbllem2.n S = dom voln X
opnvonmbllem2.g φ G TopOpen X
opnvonmbl.k K = h × X | i X . h i G
Assertion opnvonmbllem2 φ G S

Proof

Step Hyp Ref Expression
1 opnvonmbllem2.x φ X Fin
2 opnvonmbllem2.n S = dom voln X
3 opnvonmbllem2.g φ G TopOpen X
4 opnvonmbl.k K = h × X | i X . h i G
5 eqid dist X = dist X
6 5 rrxmetfi X Fin dist X Met X
7 1 6 syl φ dist X Met X
8 metxmet dist X Met X dist X ∞Met X
9 7 8 syl φ dist X ∞Met X
10 9 adantr φ x G dist X ∞Met X
11 eqid X = X
12 11 rrxval X Fin X = toCPreHil fld freeLMod X
13 1 12 syl φ X = toCPreHil fld freeLMod X
14 13 fveq2d φ TopOpen X = TopOpen toCPreHil fld freeLMod X
15 ovex fld freeLMod X V
16 eqid toCPreHil fld freeLMod X = toCPreHil fld freeLMod X
17 eqid dist toCPreHil fld freeLMod X = dist toCPreHil fld freeLMod X
18 eqid TopOpen toCPreHil fld freeLMod X = TopOpen toCPreHil fld freeLMod X
19 16 17 18 tcphtopn fld freeLMod X V TopOpen toCPreHil fld freeLMod X = MetOpen dist toCPreHil fld freeLMod X
20 15 19 ax-mp TopOpen toCPreHil fld freeLMod X = MetOpen dist toCPreHil fld freeLMod X
21 20 a1i φ TopOpen toCPreHil fld freeLMod X = MetOpen dist toCPreHil fld freeLMod X
22 13 eqcomd φ toCPreHil fld freeLMod X = X
23 22 fveq2d φ dist toCPreHil fld freeLMod X = dist X
24 23 fveq2d φ MetOpen dist toCPreHil fld freeLMod X = MetOpen dist X
25 14 21 24 3eqtrd φ TopOpen X = MetOpen dist X
26 3 25 eleqtrd φ G MetOpen dist X
27 26 adantr φ x G G MetOpen dist X
28 simpr φ x G x G
29 eqid MetOpen dist X = MetOpen dist X
30 29 mopni2 dist X ∞Met X G MetOpen dist X x G e + x ball dist X e G
31 10 27 28 30 syl3anc φ x G e + x ball dist X e G
32 1 ad2antrr φ x G e + X Fin
33 eqid TopOpen X = TopOpen X
34 33 rrxtoponfi X Fin TopOpen X TopOn X
35 1 34 syl φ TopOpen X TopOn X
36 toponss TopOpen X TopOn X G TopOpen X G X
37 35 3 36 syl2anc φ G X
38 37 adantr φ x G G X
39 38 28 sseldd φ x G x X
40 39 adantr φ x G e + x X
41 simpr φ x G e + e +
42 32 40 41 hoiqssbl φ x G e + c X d X x i X c i d i i X c i d i x ball dist X e
43 42 3adant3 φ x G e + x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e
44 nfv i φ x ball dist X e G
45 nfv i c X d X
46 nfcv _ i x
47 nfixp1 _ i i X c i d i
48 46 47 nfel i x i X c i d i
49 nfcv _ i x ball dist X e
50 47 49 nfss i i X c i d i x ball dist X e
51 48 50 nfan i x i X c i d i i X c i d i x ball dist X e
52 44 45 51 nf3an i φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e
53 1 adantr φ x ball dist X e G X Fin
54 53 3ad2ant1 φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e X Fin
55 elmapi c X c : X
56 55 adantr c X d X c : X
57 56 3ad2ant2 φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e c : X
58 elmapi d X d : X
59 58 adantl c X d X d : X
60 59 3ad2ant2 φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e d : X
61 simp3r φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e i X c i d i x ball dist X e
62 simp1r φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e x ball dist X e G
63 simp3l φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e x i X c i d i
64 eqid i X c i d i = i X c i d i
65 52 54 57 60 61 62 63 4 64 opnvonmbllem1 φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e h K x i X . h i
66 65 3exp φ x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e h K x i X . h i
67 66 adantlr φ x G x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e h K x i X . h i
68 67 3adant2 φ x G e + x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e h K x i X . h i
69 68 rexlimdvv φ x G e + x ball dist X e G c X d X x i X c i d i i X c i d i x ball dist X e h K x i X . h i
70 43 69 mpd φ x G e + x ball dist X e G h K x i X . h i
71 70 3exp φ x G e + x ball dist X e G h K x i X . h i
72 71 rexlimdv φ x G e + x ball dist X e G h K x i X . h i
73 31 72 mpd φ x G h K x i X . h i
74 eliun x h K i X . h i h K x i X . h i
75 73 74 sylibr φ x G x h K i X . h i
76 75 ralrimiva φ x G x h K i X . h i
77 dfss3 G h K i X . h i x G x h K i X . h i
78 76 77 sylibr φ G h K i X . h i
79 4 eleq2i h K h h × X | i X . h i G
80 79 biimpi h K h h × X | i X . h i G
81 80 adantl φ h K h h × X | i X . h i G
82 rabid h h × X | i X . h i G h × X i X . h i G
83 81 82 sylib φ h K h × X i X . h i G
84 83 simprd φ h K i X . h i G
85 84 ralrimiva φ h K i X . h i G
86 iunss h K i X . h i G h K i X . h i G
87 85 86 sylibr φ h K i X . h i G
88 78 87 eqssd φ G = h K i X . h i
89 1 2 dmovnsal φ S SAlg
90 ssrab2 h × X | i X . h i G × X
91 4 90 eqsstri K × X
92 91 a1i φ K × X
93 qct ω
94 93 a1i φ ω
95 xpct ω ω × ω
96 94 94 95 syl2anc φ × ω
97 96 1 mpct φ × X ω
98 ssct K × X × X ω K ω
99 92 97 98 syl2anc φ K ω
100 reex V
101 100 100 xpex 2 V
102 qssre
103 xpss12 × 2
104 102 102 103 mp2an × 2
105 mapss 2 V × 2 × X 2 X
106 101 104 105 mp2an × X 2 X
107 91 sseli h K h × X
108 106 107 sseldi h K h 2 X
109 elmapi h 2 X h : X 2
110 108 109 syl h K h : X 2
111 110 adantl φ h K h : X 2
112 2fveq3 k = i 1 st h k = 1 st h i
113 112 cbvmptv k X 1 st h k = i X 1 st h i
114 2fveq3 k = i 2 nd h k = 2 nd h i
115 114 cbvmptv k X 2 nd h k = i X 2 nd h i
116 111 113 115 hoicoto2 φ h K i X . h i = i X k X 1 st h k i k X 2 nd h k i
117 1 adantr φ h K X Fin
118 111 ffvelrnda φ h K k X h k 2
119 xp1st h k 2 1 st h k
120 118 119 syl φ h K k X 1 st h k
121 120 fmpttd φ h K k X 1 st h k : X
122 xp2nd h k 2 2 nd h k
123 118 122 syl φ h K k X 2 nd h k
124 123 fmpttd φ h K k X 2 nd h k : X
125 117 2 121 124 hoimbl φ h K i X k X 1 st h k i k X 2 nd h k i S
126 116 125 eqeltrd φ h K i X . h i S
127 89 99 126 saliuncl φ h K i X . h i S
128 88 127 eqeltrd φ G S