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

Theorem eroveu 8128
Description: Lemma for erov 8130 and eroprf 8131. (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 8085 . . . . . . . 8 (𝑋 ∈ (𝐴 / 𝑅) → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
2 eropr.1 . . . . . . . 8 𝐽 = (𝐴 / 𝑅)
31, 2eleq2s 2877 . . . . . . 7 (𝑋𝐽 → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
4 elqsi 8085 . . . . . . . 8 (𝑌 ∈ (𝐵 / 𝑆) → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
5 eropr.2 . . . . . . . 8 𝐾 = (𝐵 / 𝑆)
64, 5eleq2s 2877 . . . . . . 7 (𝑌𝐾 → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
73, 6anim12i 606 . . . . . 6 ((𝑋𝐽𝑌𝐾) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
87adantl 475 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
9 reeanv 3293 . . . . 5 (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
108, 9sylibr 226 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆))
11 eropr.3 . . . . . . . 8 (𝜑𝑇𝑍)
1211adantr 474 . . . . . . 7 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → 𝑇𝑍)
13 ecexg 8032 . . . . . . 7 (𝑇𝑍 → [(𝑝 + 𝑞)]𝑇 ∈ V)
14 elisset 3417 . . . . . . 7 ([(𝑝 + 𝑞)]𝑇 ∈ V → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1512, 13, 143syl 18 . . . . . 6 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1615biantrud 527 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
17162rexbidv 3242 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
1810, 17mpbid 224 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
19 19.42v 1996 . . . . . . . 8 (∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
2019bicomi 216 . . . . . . 7 (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2120rexbii 3224 . . . . . 6 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
22 rexcom4 3427 . . . . . 6 (∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2321, 22bitri 267 . . . . 5 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2423rexbii 3224 . . . 4 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
25 rexcom4 3427 . . . 4 (∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2624, 25bitri 267 . . 3 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2718, 26sylib 210 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
28 reeanv 3293 . . . . . 6 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
29 eceq1 8066 . . . . . . . . . . 11 (𝑝 = 𝑟 → [𝑝]𝑅 = [𝑟]𝑅)
3029eqeq2d 2788 . . . . . . . . . 10 (𝑝 = 𝑟 → (𝑋 = [𝑝]𝑅𝑋 = [𝑟]𝑅))
3130anbi1d 623 . . . . . . . . 9 (𝑝 = 𝑟 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆)))
32 oveq1 6931 . . . . . . . . . . 11 (𝑝 = 𝑟 → (𝑝 + 𝑞) = (𝑟 + 𝑞))
3332eceq1d 8067 . . . . . . . . . 10 (𝑝 = 𝑟 → [(𝑝 + 𝑞)]𝑇 = [(𝑟 + 𝑞)]𝑇)
3433eqeq2d 2788 . . . . . . . . 9 (𝑝 = 𝑟 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑞)]𝑇))
3531, 34anbi12d 624 . . . . . . . 8 (𝑝 = 𝑟 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇)))
36 eceq1 8066 . . . . . . . . . . 11 (𝑞 = 𝑡 → [𝑞]𝑆 = [𝑡]𝑆)
3736eqeq2d 2788 . . . . . . . . . 10 (𝑞 = 𝑡 → (𝑌 = [𝑞]𝑆𝑌 = [𝑡]𝑆))
3837anbi2d 622 . . . . . . . . 9 (𝑞 = 𝑡 → ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆)))
39 oveq2 6932 . . . . . . . . . . 11 (𝑞 = 𝑡 → (𝑟 + 𝑞) = (𝑟 + 𝑡))
4039eceq1d 8067 . . . . . . . . . 10 (𝑞 = 𝑡 → [(𝑟 + 𝑞)]𝑇 = [(𝑟 + 𝑡)]𝑇)
4140eqeq2d 2788 . . . . . . . . 9 (𝑞 = 𝑡 → (𝑧 = [(𝑟 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑡)]𝑇))
4238, 41anbi12d 624 . . . . . . . 8 (𝑞 = 𝑡 → (((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇)))
4335, 42cbvrex2v 3376 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇))
44 eceq1 8066 . . . . . . . . . . 11 (𝑝 = 𝑠 → [𝑝]𝑅 = [𝑠]𝑅)
4544eqeq2d 2788 . . . . . . . . . 10 (𝑝 = 𝑠 → (𝑋 = [𝑝]𝑅𝑋 = [𝑠]𝑅))
4645anbi1d 623 . . . . . . . . 9 (𝑝 = 𝑠 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆)))
47 oveq1 6931 . . . . . . . . . . 11 (𝑝 = 𝑠 → (𝑝 + 𝑞) = (𝑠 + 𝑞))
4847eceq1d 8067 . . . . . . . . . 10 (𝑝 = 𝑠 → [(𝑝 + 𝑞)]𝑇 = [(𝑠 + 𝑞)]𝑇)
4948eqeq2d 2788 . . . . . . . . 9 (𝑝 = 𝑠 → (𝑤 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑞)]𝑇))
5046, 49anbi12d 624 . . . . . . . 8 (𝑝 = 𝑠 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇)))
51 eceq1 8066 . . . . . . . . . . 11 (𝑞 = 𝑢 → [𝑞]𝑆 = [𝑢]𝑆)
5251eqeq2d 2788 . . . . . . . . . 10 (𝑞 = 𝑢 → (𝑌 = [𝑞]𝑆𝑌 = [𝑢]𝑆))
5352anbi2d 622 . . . . . . . . 9 (𝑞 = 𝑢 → ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆)))
54 oveq2 6932 . . . . . . . . . . 11 (𝑞 = 𝑢 → (𝑠 + 𝑞) = (𝑠 + 𝑢))
5554eceq1d 8067 . . . . . . . . . 10 (𝑞 = 𝑢 → [(𝑠 + 𝑞)]𝑇 = [(𝑠 + 𝑢)]𝑇)
5655eqeq2d 2788 . . . . . . . . 9 (𝑞 = 𝑢 → (𝑤 = [(𝑠 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑢)]𝑇))
5753, 56anbi12d 624 . . . . . . . 8 (𝑞 = 𝑢 → (((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
5850, 57cbvrex2v 3376 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))
5943, 58anbi12i 620 . . . . . 6 ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
6028, 59bitr4i 270 . . . . 5 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
61 reeanv 3293 . . . . . . 7 (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
62 eropr.11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))
63 eropr.4 . . . . . . . . . . . . . . . . 17 (𝜑𝑅 Er 𝑈)
6463adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑅 Er 𝑈)
65 eropr.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴𝑈)
6665adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐴𝑈)
67 simprll 769 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝐴)
6866, 67sseldd 3822 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝑈)
6964, 68erth 8075 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟𝑅𝑠 ↔ [𝑟]𝑅 = [𝑠]𝑅))
70 eropr.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Er 𝑉)
7170adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑆 Er 𝑉)
72 eropr.8 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵𝑉)
7372adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐵𝑉)
74 simprrl 771 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝐵)
7573, 74sseldd 3822 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝑉)
7671, 75erth 8075 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑡𝑆𝑢 ↔ [𝑡]𝑆 = [𝑢]𝑆))
7769, 76anbi12d 624 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
78 eropr.6 . . . . . . . . . . . . . . . 16 (𝜑𝑇 Er 𝑊)
7978adantr 474 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑇 Er 𝑊)
80 eropr.9 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝑊)
8180adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐶𝑊)
82 eropr.10 . . . . . . . . . . . . . . . . . 18 (𝜑+ :(𝐴 × 𝐵)⟶𝐶)
8382adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → + :(𝐴 × 𝐵)⟶𝐶)
8483, 67, 74fovrnd 7085 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝐶)
8581, 84sseldd 3822 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝑊)
8679, 85erth 8075 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟 + 𝑡)𝑇(𝑠 + 𝑢) ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8762, 77, 863imtr3d 285 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
88 eqeq2 2789 . . . . . . . . . . . . . 14 (𝑤 = [(𝑠 + 𝑢)]𝑇 → ([(𝑟 + 𝑡)]𝑇 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8988biimprcd 242 . . . . . . . . . . . . 13 ([(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇 → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤))
9087, 89syl6 35 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
9190impd 400 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤))
92 eqeq1 2782 . . . . . . . . . . . . . . 15 (𝑋 = [𝑟]𝑅 → (𝑋 = [𝑠]𝑅 ↔ [𝑟]𝑅 = [𝑠]𝑅))
93 eqeq1 2782 . . . . . . . . . . . . . . 15 (𝑌 = [𝑡]𝑆 → (𝑌 = [𝑢]𝑆 ↔ [𝑡]𝑆 = [𝑢]𝑆))
9492, 93bi2anan9 629 . . . . . . . . . . . . . 14 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
9594anbi1d 623 . . . . . . . . . . . . 13 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
9695adantr 474 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
97 eqeq1 2782 . . . . . . . . . . . . 13 (𝑧 = [(𝑟 + 𝑡)]𝑇 → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9897adantl 475 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9996, 98imbi12d 336 . . . . . . . . . . 11 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → ((((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤) ↔ ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
10091, 99syl5ibrcom 239 . . . . . . . . . 10 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤)))
101100impd 400 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
102101anassrs 461 . . . . . . . 8 (((𝜑 ∧ (𝑟𝐴𝑠𝐴)) ∧ (𝑡𝐵𝑢𝐵)) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
103102rexlimdvva 3221 . . . . . . 7 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10461, 103syl5bir 235 . . . . . 6 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → ((∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
105104rexlimdvva 3221 . . . . 5 (𝜑 → (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10660, 105syl5bir 235 . . . 4 (𝜑 → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
107106adantr 474 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
108107alrimivv 1971 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
109 eqeq1 2782 . . . . 5 (𝑧 = 𝑤 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑝 + 𝑞)]𝑇))
110109anbi2d 622 . . . 4 (𝑧 = 𝑤 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
1111102rexbidv 3242 . . 3 (𝑧 = 𝑤 → (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
112111eu4 2650 . 2 (∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ (∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤)))
11327, 108, 112sylanbrc 578 1 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wal 1599   = wceq 1601  wex 1823  wcel 2107  ∃!weu 2586  wrex 3091  Vcvv 3398  wss 3792   class class class wbr 4888   × cxp 5355  wf 6133  (class class class)co 6924   Er wer 8025  [cec 8026   / cqs 8027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140  ax-un 7228
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-fv 6145  df-ov 6927  df-er 8028  df-ec 8030  df-qs 8034
This theorem is referenced by:  erovlem  8129  erov  8130  eroprf  8131
  Copyright terms: Public domain W3C validator