This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
genpcl.3 ⊢ ( ℎ ∈ Q → ( 𝑓 <Q 𝑔 ↔ ( ℎ 𝐺 𝑓 ) <Q ( ℎ 𝐺 𝑔 ) ) )
genpcl.4 ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
genpcl.5 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 𝐺 ℎ ) → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) )
Assertion genpcl ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) ∈ P )

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 genpcl.3 ⊢ ( ℎ ∈ Q → ( 𝑓 <Q 𝑔 ↔ ( ℎ 𝐺 𝑓 ) <Q ( ℎ 𝐺 𝑔 ) ) )
4 genpcl.4 ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
5 genpcl.5 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 𝐺 ℎ ) → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) )
6 1 2 genpn0 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) )
7 1 2 genpss ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) ⊆ Q )
8 vex ⊢ 𝑥 ∈ V
9 vex ⊢ 𝑦 ∈ V
10 8 9 3 caovord ⊢ ( 𝑧 ∈ Q → ( 𝑥 <Q 𝑦 ↔ ( 𝑧 𝐺 𝑥 ) <Q ( 𝑧 𝐺 𝑦 ) ) )
11 1 2 10 4 genpnnp ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ¬ ( 𝐴 𝐹 𝐵 ) = Q )
12 dfpss2 ⊢ ( ( 𝐴 𝐹 𝐵 ) ⊊ Q ↔ ( ( 𝐴 𝐹 𝐵 ) ⊆ Q ∧ ¬ ( 𝐴 𝐹 𝐵 ) = Q ) )
13 7 11 12 sylanbrc ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) ⊊ Q )
14 1 2 5 genpcd ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) )
15 14 alrimdv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ∀ 𝑥 ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) )
16 vex ⊢ 𝑧 ∈ V
17 vex ⊢ 𝑤 ∈ V
18 16 17 3 caovord ⊢ ( 𝑣 ∈ Q → ( 𝑧 <Q 𝑤 ↔ ( 𝑣 𝐺 𝑧 ) <Q ( 𝑣 𝐺 𝑤 ) ) )
19 16 17 4 caovcom ⊢ ( 𝑧 𝐺 𝑤 ) = ( 𝑤 𝐺 𝑧 )
20 1 2 18 19 genpnmax ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) )
21 15 20 jcad ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ( ∀ 𝑥 ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ∧ ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) ) )
22 21 ralrimiv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ∀ 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) ( ∀ 𝑥 ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ∧ ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) )
23 elnp ⊢ ( ( 𝐴 𝐹 𝐵 ) ∈ P ↔ ( ( ∅ ⊊ ( 𝐴 𝐹 𝐵 ) ∧ ( 𝐴 𝐹 𝐵 ) ⊊ Q ) ∧ ∀ 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) ( ∀ 𝑥 ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ∧ ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) ) )
24 6 13 22 23 syl21anbrc ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) ∈ P )