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 ∈ v x = y G z
genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
genpcl.3 ⊢ h ∈ 𝑸 → f < 𝑸 g ↔ h G f < 𝑸 h G g
genpcl.4 ⊢ x G y = y G x
genpcl.5 ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B ∧ x ∈ 𝑸 → x < 𝑸 g G h → x ∈ A F B
Assertion genpcl ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A F B ∈ 𝑷

Proof

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