Metamath Proof Explorer


Theorem erovlem

Description: Lemma for erov and eroprf . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses eropr.1 𝐽 = ( 𝐴 / 𝑅 )
eropr.2 𝐾 = ( 𝐵 / 𝑆 )
eropr.3 ( 𝜑𝑇𝑍 )
eropr.4 ( 𝜑𝑅 Er 𝑈 )
eropr.5 ( 𝜑𝑆 Er 𝑉 )
eropr.6 ( 𝜑𝑇 Er 𝑊 )
eropr.7 ( 𝜑𝐴𝑈 )
eropr.8 ( 𝜑𝐵𝑉 )
eropr.9 ( 𝜑𝐶𝑊 )
eropr.10 ( 𝜑+ : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
eropr.11 ( ( 𝜑 ∧ ( ( 𝑟𝐴𝑠𝐴 ) ∧ ( 𝑡𝐵𝑢𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
eropr.12 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) }
Assertion erovlem ( 𝜑 = ( 𝑥𝐽 , 𝑦𝐾 ↦ ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )

Proof

Step Hyp Ref Expression
1 eropr.1 𝐽 = ( 𝐴 / 𝑅 )
2 eropr.2 𝐾 = ( 𝐵 / 𝑆 )
3 eropr.3 ( 𝜑𝑇𝑍 )
4 eropr.4 ( 𝜑𝑅 Er 𝑈 )
5 eropr.5 ( 𝜑𝑆 Er 𝑉 )
6 eropr.6 ( 𝜑𝑇 Er 𝑊 )
7 eropr.7 ( 𝜑𝐴𝑈 )
8 eropr.8 ( 𝜑𝐵𝑉 )
9 eropr.9 ( 𝜑𝐶𝑊 )
10 eropr.10 ( 𝜑+ : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
11 eropr.11 ( ( 𝜑 ∧ ( ( 𝑟𝐴𝑠𝐴 ) ∧ ( 𝑡𝐵𝑢𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
12 eropr.12 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) }
13 simpl ( ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) )
14 13 reximi ( ∃ 𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ∃ 𝑞𝐵 ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) )
15 14 reximi ( ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ∃ 𝑝𝐴𝑞𝐵 ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) )
16 1 eleq2i ( 𝑥𝐽𝑥 ∈ ( 𝐴 / 𝑅 ) )
17 vex 𝑥 ∈ V
18 17 elqs ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑝𝐴 𝑥 = [ 𝑝 ] 𝑅 )
19 16 18 bitri ( 𝑥𝐽 ↔ ∃ 𝑝𝐴 𝑥 = [ 𝑝 ] 𝑅 )
20 2 eleq2i ( 𝑦𝐾𝑦 ∈ ( 𝐵 / 𝑆 ) )
21 vex 𝑦 ∈ V
22 21 elqs ( 𝑦 ∈ ( 𝐵 / 𝑆 ) ↔ ∃ 𝑞𝐵 𝑦 = [ 𝑞 ] 𝑆 )
23 20 22 bitri ( 𝑦𝐾 ↔ ∃ 𝑞𝐵 𝑦 = [ 𝑞 ] 𝑆 )
24 19 23 anbi12i ( ( 𝑥𝐽𝑦𝐾 ) ↔ ( ∃ 𝑝𝐴 𝑥 = [ 𝑝 ] 𝑅 ∧ ∃ 𝑞𝐵 𝑦 = [ 𝑞 ] 𝑆 ) )
25 reeanv ( ∃ 𝑝𝐴𝑞𝐵 ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ↔ ( ∃ 𝑝𝐴 𝑥 = [ 𝑝 ] 𝑅 ∧ ∃ 𝑞𝐵 𝑦 = [ 𝑞 ] 𝑆 ) )
26 24 25 bitr4i ( ( 𝑥𝐽𝑦𝐾 ) ↔ ∃ 𝑝𝐴𝑞𝐵 ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) )
27 15 26 sylibr ( ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ( 𝑥𝐽𝑦𝐾 ) )
28 27 pm4.71ri ( ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑥𝐽𝑦𝐾 ) ∧ ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
29 1 2 3 4 5 6 7 8 9 10 11 eroveu ( ( 𝜑 ∧ ( 𝑥𝐽𝑦𝐾 ) ) → ∃! 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
30 iota1 ( ∃! 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ( ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = 𝑧 ) )
31 29 30 syl ( ( 𝜑 ∧ ( 𝑥𝐽𝑦𝐾 ) ) → ( ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = 𝑧 ) )
32 eqcom ( ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = 𝑧𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
33 31 32 syl6bb ( ( 𝜑 ∧ ( 𝑥𝐽𝑦𝐾 ) ) → ( ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )
34 33 pm5.32da ( 𝜑 → ( ( ( 𝑥𝐽𝑦𝐾 ) ∧ ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ↔ ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ) )
35 28 34 syl5bb ( 𝜑 → ( ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ) )
36 35 oprabbidv ( 𝜑 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) } )
37 df-mpo ( 𝑥𝐽 , 𝑦𝐾 ↦ ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑤 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) }
38 nfv 𝑤 ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
39 nfv 𝑧 ( 𝑥𝐽𝑦𝐾 )
40 nfiota1 𝑧 ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
41 40 nfeq2 𝑧 𝑤 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
42 39 41 nfan 𝑧 ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑤 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
43 eqeq1 ( 𝑧 = 𝑤 → ( 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ↔ 𝑤 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )
44 43 anbi2d ( 𝑧 = 𝑤 → ( ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ↔ ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑤 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ) )
45 38 42 44 cbvoprab3 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑤 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) }
46 37 45 eqtr4i ( 𝑥𝐽 , 𝑦𝐾 ↦ ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐽𝑦𝐾 ) ∧ 𝑧 = ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) }
47 36 12 46 3eqtr4g ( 𝜑 = ( 𝑥𝐽 , 𝑦𝐾 ↦ ( ℩ 𝑧𝑝𝐴𝑞𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )