Metamath Proof Explorer

Theorem genpcl

Description: Closure of an operation on reals. (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 ⊢F=w∈𝑷,v∈𝑷⟼x|∃y∈w∃z∈vx=yGz
genp.2 ⊢y∈𝑸∧z∈𝑸→yGz∈𝑸
genpcl.3 ⊢h∈𝑸→f<𝑸g↔hGf<𝑸hGg
genpcl.4 ⊢xGy=yGx
genpcl.5 ⊢A∈𝑷∧g∈A∧B∈𝑷∧h∈B∧x∈𝑸→x<𝑸gGh→x∈AFB
Assertion genpcl ⊢A∈𝑷∧B∈𝑷→AFB∈𝑷

Proof

Step Hyp Ref Expression
1 genp.1 ⊢F=w∈𝑷,v∈𝑷⟼x|∃y∈w∃z∈vx=yGz
2 genp.2 ⊢y∈𝑸∧z∈𝑸→yGz∈𝑸
3 genpcl.3 ⊢h∈𝑸→f<𝑸g↔hGf<𝑸hGg
4 genpcl.4 ⊢xGy=yGx
5 genpcl.5 ⊢A∈𝑷∧g∈A∧B∈𝑷∧h∈B∧x∈𝑸→x<𝑸gGh→x∈AFB
6 1 2 genpn0 ⊢A∈𝑷∧B∈𝑷→∅⊂AFB
7 1 2 genpss ⊢A∈𝑷∧B∈𝑷→AFB⊆𝑸
8 vex ⊢x∈V
9 vex ⊢y∈V
10 8 9 3 caovord ⊢z∈𝑸→x<𝑸y↔zGx<𝑸zGy
11 1 2 10 4 genpnnp ⊢A∈𝑷∧B∈𝑷→¬AFB=𝑸
12 dfpss2 ⊢AFB⊂𝑸↔AFB⊆𝑸∧¬AFB=𝑸
13 7 11 12 sylanbrc ⊢A∈𝑷∧B∈𝑷→AFB⊂𝑸
14 1 2 5 genpcd ⊢A∈𝑷∧B∈𝑷→f∈AFB→x<𝑸f→x∈AFB
15 14 alrimdv ⊢A∈𝑷∧B∈𝑷→f∈AFB→∀xx<𝑸f→x∈AFB
16 vex ⊢z∈V
17 vex ⊢w∈V
18 16 17 3 caovord ⊢v∈𝑸→z<𝑸w↔vGz<𝑸vGw
19 16 17 4 caovcom ⊢zGw=wGz
20 1 2 18 19 genpnmax ⊢A∈𝑷∧B∈𝑷→f∈AFB→∃x∈AFBf<𝑸x
21 15 20 jcad ⊢A∈𝑷∧B∈𝑷→f∈AFB→∀xx<𝑸f→x∈AFB∧∃x∈AFBf<𝑸x
22 21 ralrimiv ⊢A∈𝑷∧B∈𝑷→∀f∈AFB∀xx<𝑸f→x∈AFB∧∃x∈AFBf<𝑸x
23 elnp ⊢AFB∈𝑷↔∅⊂AFB∧AFB⊂𝑸∧∀f∈AFB∀xx<𝑸f→x∈AFB∧∃x∈AFBf<𝑸x
24 6 13 22 23 syl21anbrc ⊢A∈𝑷∧B∈𝑷→AFB∈𝑷