MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eroveu Structured version   Visualization version   GIF version

Theorem eroveu 8584
Description: Lemma for erov 8586 and eroprf 8587. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
Hypotheses
Ref Expression
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 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))
Assertion
Ref Expression
eroveu ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Distinct variable groups:   𝑞,𝑝,𝑟,𝑠,𝑡,𝑢,𝑧,𝐴   𝐵,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝐽,𝑝,𝑞,𝑧   𝑅,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝐾,𝑝,𝑞,𝑧   𝑆,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   + ,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝜑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝑇,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝑋,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝑌,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧
Allowed substitution hints:   𝐶(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑈(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)   𝐽(𝑢,𝑡,𝑠,𝑟)   𝐾(𝑢,𝑡,𝑠,𝑟)   𝑉(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑊(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑍(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)

Proof of Theorem eroveu
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 elqsi 8542 . . . . . . . 8 (𝑋 ∈ (𝐴 / 𝑅) → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
2 eropr.1 . . . . . . . 8 𝐽 = (𝐴 / 𝑅)
31, 2eleq2s 2859 . . . . . . 7 (𝑋𝐽 → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
4 elqsi 8542 . . . . . . . 8 (𝑌 ∈ (𝐵 / 𝑆) → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
5 eropr.2 . . . . . . . 8 𝐾 = (𝐵 / 𝑆)
64, 5eleq2s 2859 . . . . . . 7 (𝑌𝐾 → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
73, 6anim12i 613 . . . . . 6 ((𝑋𝐽𝑌𝐾) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
87adantl 482 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
9 reeanv 3295 . . . . 5 (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
108, 9sylibr 233 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆))
11 eropr.3 . . . . . . . 8 (𝜑𝑇𝑍)
1211adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → 𝑇𝑍)
13 ecexg 8485 . . . . . . 7 (𝑇𝑍 → [(𝑝 + 𝑞)]𝑇 ∈ V)
14 elisset 2822 . . . . . . 7 ([(𝑝 + 𝑞)]𝑇 ∈ V → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1512, 13, 143syl 18 . . . . . 6 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1615biantrud 532 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
17162rexbidv 3231 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
1810, 17mpbid 231 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
19 19.42v 1961 . . . . . . . 8 (∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
2019bicomi 223 . . . . . . 7 (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2120rexbii 3180 . . . . . 6 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
22 rexcom4 3182 . . . . . 6 (∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2321, 22bitri 274 . . . . 5 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2423rexbii 3180 . . . 4 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
25 rexcom4 3182 . . . 4 (∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2624, 25bitri 274 . . 3 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2718, 26sylib 217 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
28 reeanv 3295 . . . . . 6 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
29 eceq1 8519 . . . . . . . . . . 11 (𝑝 = 𝑟 → [𝑝]𝑅 = [𝑟]𝑅)
3029eqeq2d 2751 . . . . . . . . . 10 (𝑝 = 𝑟 → (𝑋 = [𝑝]𝑅𝑋 = [𝑟]𝑅))
3130anbi1d 630 . . . . . . . . 9 (𝑝 = 𝑟 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆)))
32 oveq1 7278 . . . . . . . . . . 11 (𝑝 = 𝑟 → (𝑝 + 𝑞) = (𝑟 + 𝑞))
3332eceq1d 8520 . . . . . . . . . 10 (𝑝 = 𝑟 → [(𝑝 + 𝑞)]𝑇 = [(𝑟 + 𝑞)]𝑇)
3433eqeq2d 2751 . . . . . . . . 9 (𝑝 = 𝑟 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑞)]𝑇))
3531, 34anbi12d 631 . . . . . . . 8 (𝑝 = 𝑟 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇)))
36 eceq1 8519 . . . . . . . . . . 11 (𝑞 = 𝑡 → [𝑞]𝑆 = [𝑡]𝑆)
3736eqeq2d 2751 . . . . . . . . . 10 (𝑞 = 𝑡 → (𝑌 = [𝑞]𝑆𝑌 = [𝑡]𝑆))
3837anbi2d 629 . . . . . . . . 9 (𝑞 = 𝑡 → ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆)))
39 oveq2 7279 . . . . . . . . . . 11 (𝑞 = 𝑡 → (𝑟 + 𝑞) = (𝑟 + 𝑡))
4039eceq1d 8520 . . . . . . . . . 10 (𝑞 = 𝑡 → [(𝑟 + 𝑞)]𝑇 = [(𝑟 + 𝑡)]𝑇)
4140eqeq2d 2751 . . . . . . . . 9 (𝑞 = 𝑡 → (𝑧 = [(𝑟 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑡)]𝑇))
4238, 41anbi12d 631 . . . . . . . 8 (𝑞 = 𝑡 → (((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇)))
4335, 42cbvrex2vw 3395 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇))
44 eceq1 8519 . . . . . . . . . . 11 (𝑝 = 𝑠 → [𝑝]𝑅 = [𝑠]𝑅)
4544eqeq2d 2751 . . . . . . . . . 10 (𝑝 = 𝑠 → (𝑋 = [𝑝]𝑅𝑋 = [𝑠]𝑅))
4645anbi1d 630 . . . . . . . . 9 (𝑝 = 𝑠 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆)))
47 oveq1 7278 . . . . . . . . . . 11 (𝑝 = 𝑠 → (𝑝 + 𝑞) = (𝑠 + 𝑞))
4847eceq1d 8520 . . . . . . . . . 10 (𝑝 = 𝑠 → [(𝑝 + 𝑞)]𝑇 = [(𝑠 + 𝑞)]𝑇)
4948eqeq2d 2751 . . . . . . . . 9 (𝑝 = 𝑠 → (𝑤 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑞)]𝑇))
5046, 49anbi12d 631 . . . . . . . 8 (𝑝 = 𝑠 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇)))
51 eceq1 8519 . . . . . . . . . . 11 (𝑞 = 𝑢 → [𝑞]𝑆 = [𝑢]𝑆)
5251eqeq2d 2751 . . . . . . . . . 10 (𝑞 = 𝑢 → (𝑌 = [𝑞]𝑆𝑌 = [𝑢]𝑆))
5352anbi2d 629 . . . . . . . . 9 (𝑞 = 𝑢 → ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆)))
54 oveq2 7279 . . . . . . . . . . 11 (𝑞 = 𝑢 → (𝑠 + 𝑞) = (𝑠 + 𝑢))
5554eceq1d 8520 . . . . . . . . . 10 (𝑞 = 𝑢 → [(𝑠 + 𝑞)]𝑇 = [(𝑠 + 𝑢)]𝑇)
5655eqeq2d 2751 . . . . . . . . 9 (𝑞 = 𝑢 → (𝑤 = [(𝑠 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑢)]𝑇))
5753, 56anbi12d 631 . . . . . . . 8 (𝑞 = 𝑢 → (((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
5850, 57cbvrex2vw 3395 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))
5943, 58anbi12i 627 . . . . . 6 ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
6028, 59bitr4i 277 . . . . 5 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
61 reeanv 3295 . . . . . . 7 (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
62 eropr.11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))
63 eropr.4 . . . . . . . . . . . . . . . . 17 (𝜑𝑅 Er 𝑈)
6463adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑅 Er 𝑈)
65 eropr.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴𝑈)
6665adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐴𝑈)
67 simprll 776 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝐴)
6866, 67sseldd 3927 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝑈)
6964, 68erth 8530 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟𝑅𝑠 ↔ [𝑟]𝑅 = [𝑠]𝑅))
70 eropr.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Er 𝑉)
7170adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑆 Er 𝑉)
72 eropr.8 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵𝑉)
7372adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐵𝑉)
74 simprrl 778 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝐵)
7573, 74sseldd 3927 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝑉)
7671, 75erth 8530 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑡𝑆𝑢 ↔ [𝑡]𝑆 = [𝑢]𝑆))
7769, 76anbi12d 631 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
78 eropr.6 . . . . . . . . . . . . . . . 16 (𝜑𝑇 Er 𝑊)
7978adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑇 Er 𝑊)
80 eropr.9 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝑊)
8180adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐶𝑊)
82 eropr.10 . . . . . . . . . . . . . . . . . 18 (𝜑+ :(𝐴 × 𝐵)⟶𝐶)
8382adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → + :(𝐴 × 𝐵)⟶𝐶)
8483, 67, 74fovrnd 7438 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝐶)
8581, 84sseldd 3927 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝑊)
8679, 85erth 8530 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟 + 𝑡)𝑇(𝑠 + 𝑢) ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8762, 77, 863imtr3d 293 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
88 eqeq2 2752 . . . . . . . . . . . . . 14 (𝑤 = [(𝑠 + 𝑢)]𝑇 → ([(𝑟 + 𝑡)]𝑇 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8988biimprcd 249 . . . . . . . . . . . . 13 ([(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇 → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤))
9087, 89syl6 35 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
9190impd 411 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤))
92 eqeq1 2744 . . . . . . . . . . . . . . 15 (𝑋 = [𝑟]𝑅 → (𝑋 = [𝑠]𝑅 ↔ [𝑟]𝑅 = [𝑠]𝑅))
93 eqeq1 2744 . . . . . . . . . . . . . . 15 (𝑌 = [𝑡]𝑆 → (𝑌 = [𝑢]𝑆 ↔ [𝑡]𝑆 = [𝑢]𝑆))
9492, 93bi2anan9 636 . . . . . . . . . . . . . 14 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
9594anbi1d 630 . . . . . . . . . . . . 13 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
9695adantr 481 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
97 eqeq1 2744 . . . . . . . . . . . . 13 (𝑧 = [(𝑟 + 𝑡)]𝑇 → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9897adantl 482 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9996, 98imbi12d 345 . . . . . . . . . . 11 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → ((((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤) ↔ ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
10091, 99syl5ibrcom 246 . . . . . . . . . 10 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤)))
101100impd 411 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
102101anassrs 468 . . . . . . . 8 (((𝜑 ∧ (𝑟𝐴𝑠𝐴)) ∧ (𝑡𝐵𝑢𝐵)) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
103102rexlimdvva 3225 . . . . . . 7 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10461, 103syl5bir 242 . . . . . 6 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → ((∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
105104rexlimdvva 3225 . . . . 5 (𝜑 → (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10660, 105syl5bir 242 . . . 4 (𝜑 → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
107106adantr 481 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
108107alrimivv 1935 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
109 eqeq1 2744 . . . . 5 (𝑧 = 𝑤 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑝 + 𝑞)]𝑇))
110109anbi2d 629 . . . 4 (𝑧 = 𝑤 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
1111102rexbidv 3231 . . 3 (𝑧 = 𝑤 → (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
112111eu4 2619 . 2 (∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ (∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤)))
11327, 108, 112sylanbrc 583 1 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1540   = wceq 1542  wex 1786  wcel 2110  ∃!weu 2570  wrex 3067  Vcvv 3431  wss 3892   class class class wbr 5079   × cxp 5588  wf 6428  (class class class)co 7271   Er wer 8478  [cec 8479   / cqs 8480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-fv 6440  df-ov 7274  df-er 8481  df-ec 8483  df-qs 8487
This theorem is referenced by:  erovlem  8585  erov  8586  eroprf  8587
  Copyright terms: Public domain W3C validator