Metamath Proof Explorer

Theorem genpcd

Description: Downward closure of an operation on positive reals. (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
genpcd.2 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 𝐺 ℎ ) → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) )
Assertion genpcd ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 genpcd.2 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 𝐺 ℎ ) → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) )
4 ltrelnq ⊢ <Q ⊆ ( Q × Q )
5 4 brel ⊢ ( 𝑥 <Q 𝑓 → ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) )
6 5 simpld ⊢ ( 𝑥 <Q 𝑓 → 𝑥 ∈ Q )
7 1 2 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) ) )
8 7 adantr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝑥 ∈ Q ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) ) )
9 breq2 ⊢ ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ( 𝑥 <Q 𝑓 ↔ 𝑥 <Q ( 𝑔 𝐺 ℎ ) ) )
10 9 biimpd ⊢ ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ( 𝑥 <Q 𝑓 → 𝑥 <Q ( 𝑔 𝐺 ℎ ) ) )
11 10 3 sylan9r ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) ∧ 𝑓 = ( 𝑔 𝐺 ℎ ) ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) )
12 11 exp31 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( 𝑥 ∈ Q → ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) ) )
13 12 an4s ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( 𝑥 ∈ Q → ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) ) )
14 13 impancom ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝑥 ∈ Q ) → ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) ) )
15 14 rexlimdvv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝑥 ∈ Q ) → ( ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) )
16 8 15 sylbid ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝑥 ∈ Q ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) )
17 16 ex ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑥 ∈ Q → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) ) )
18 6 17 syl5 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑥 <Q 𝑓 → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) ) )
19 18 com34 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑥 <Q 𝑓 → ( 𝑥 <Q 𝑓 → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) ) )
20 19 pm2.43d ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑥 <Q 𝑓 → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) )
21 20 com23 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ) ) )