ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eroveu GIF version

Theorem eroveu 6616
Description: Lemma for eroprf 6618. (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 6577 . . . . . . . 8 (𝑋 ∈ (𝐴 / 𝑅) → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
2 eropr.1 . . . . . . . 8 𝐽 = (𝐴 / 𝑅)
31, 2eleq2s 2270 . . . . . . 7 (𝑋𝐽 → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
4 elqsi 6577 . . . . . . . 8 (𝑌 ∈ (𝐵 / 𝑆) → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
5 eropr.2 . . . . . . . 8 𝐾 = (𝐵 / 𝑆)
64, 5eleq2s 2270 . . . . . . 7 (𝑌𝐾 → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
73, 6anim12i 338 . . . . . 6 ((𝑋𝐽𝑌𝐾) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
87adantl 277 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
9 reeanv 2644 . . . . 5 (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
108, 9sylibr 134 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆))
11 eropr.3 . . . . . . . 8 (𝜑𝑇𝑍)
1211adantr 276 . . . . . . 7 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → 𝑇𝑍)
13 ecexg 6529 . . . . . . 7 (𝑇𝑍 → [(𝑝 + 𝑞)]𝑇 ∈ V)
14 elisset 2749 . . . . . . 7 ([(𝑝 + 𝑞)]𝑇 ∈ V → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1512, 13, 143syl 17 . . . . . 6 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1615biantrud 304 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
17162rexbidv 2500 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
1810, 17mpbid 147 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
19 19.42v 1904 . . . . . . . 8 (∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
2019bicomi 132 . . . . . . 7 (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2120rexbii 2482 . . . . . 6 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
22 rexcom4 2758 . . . . . 6 (∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2321, 22bitri 184 . . . . 5 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2423rexbii 2482 . . . 4 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
25 rexcom4 2758 . . . 4 (∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2624, 25bitri 184 . . 3 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2718, 26sylib 122 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
28 reeanv 2644 . . . . . 6 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
29 eceq1 6560 . . . . . . . . . . 11 (𝑝 = 𝑟 → [𝑝]𝑅 = [𝑟]𝑅)
3029eqeq2d 2187 . . . . . . . . . 10 (𝑝 = 𝑟 → (𝑋 = [𝑝]𝑅𝑋 = [𝑟]𝑅))
3130anbi1d 465 . . . . . . . . 9 (𝑝 = 𝑟 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆)))
32 oveq1 5872 . . . . . . . . . . 11 (𝑝 = 𝑟 → (𝑝 + 𝑞) = (𝑟 + 𝑞))
3332eceq1d 6561 . . . . . . . . . 10 (𝑝 = 𝑟 → [(𝑝 + 𝑞)]𝑇 = [(𝑟 + 𝑞)]𝑇)
3433eqeq2d 2187 . . . . . . . . 9 (𝑝 = 𝑟 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑞)]𝑇))
3531, 34anbi12d 473 . . . . . . . 8 (𝑝 = 𝑟 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇)))
36 eceq1 6560 . . . . . . . . . . 11 (𝑞 = 𝑡 → [𝑞]𝑆 = [𝑡]𝑆)
3736eqeq2d 2187 . . . . . . . . . 10 (𝑞 = 𝑡 → (𝑌 = [𝑞]𝑆𝑌 = [𝑡]𝑆))
3837anbi2d 464 . . . . . . . . 9 (𝑞 = 𝑡 → ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆)))
39 oveq2 5873 . . . . . . . . . . 11 (𝑞 = 𝑡 → (𝑟 + 𝑞) = (𝑟 + 𝑡))
4039eceq1d 6561 . . . . . . . . . 10 (𝑞 = 𝑡 → [(𝑟 + 𝑞)]𝑇 = [(𝑟 + 𝑡)]𝑇)
4140eqeq2d 2187 . . . . . . . . 9 (𝑞 = 𝑡 → (𝑧 = [(𝑟 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑡)]𝑇))
4238, 41anbi12d 473 . . . . . . . 8 (𝑞 = 𝑡 → (((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇)))
4335, 42cbvrex2v 2715 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇))
44 eceq1 6560 . . . . . . . . . . 11 (𝑝 = 𝑠 → [𝑝]𝑅 = [𝑠]𝑅)
4544eqeq2d 2187 . . . . . . . . . 10 (𝑝 = 𝑠 → (𝑋 = [𝑝]𝑅𝑋 = [𝑠]𝑅))
4645anbi1d 465 . . . . . . . . 9 (𝑝 = 𝑠 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆)))
47 oveq1 5872 . . . . . . . . . . 11 (𝑝 = 𝑠 → (𝑝 + 𝑞) = (𝑠 + 𝑞))
4847eceq1d 6561 . . . . . . . . . 10 (𝑝 = 𝑠 → [(𝑝 + 𝑞)]𝑇 = [(𝑠 + 𝑞)]𝑇)
4948eqeq2d 2187 . . . . . . . . 9 (𝑝 = 𝑠 → (𝑤 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑞)]𝑇))
5046, 49anbi12d 473 . . . . . . . 8 (𝑝 = 𝑠 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇)))
51 eceq1 6560 . . . . . . . . . . 11 (𝑞 = 𝑢 → [𝑞]𝑆 = [𝑢]𝑆)
5251eqeq2d 2187 . . . . . . . . . 10 (𝑞 = 𝑢 → (𝑌 = [𝑞]𝑆𝑌 = [𝑢]𝑆))
5352anbi2d 464 . . . . . . . . 9 (𝑞 = 𝑢 → ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆)))
54 oveq2 5873 . . . . . . . . . . 11 (𝑞 = 𝑢 → (𝑠 + 𝑞) = (𝑠 + 𝑢))
5554eceq1d 6561 . . . . . . . . . 10 (𝑞 = 𝑢 → [(𝑠 + 𝑞)]𝑇 = [(𝑠 + 𝑢)]𝑇)
5655eqeq2d 2187 . . . . . . . . 9 (𝑞 = 𝑢 → (𝑤 = [(𝑠 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑢)]𝑇))
5753, 56anbi12d 473 . . . . . . . 8 (𝑞 = 𝑢 → (((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
5850, 57cbvrex2v 2715 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))
5943, 58anbi12i 460 . . . . . 6 ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
6028, 59bitr4i 187 . . . . 5 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
61 reeanv 2644 . . . . . . 7 (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
62 eropr.11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))
63 eropr.4 . . . . . . . . . . . . . . . . 17 (𝜑𝑅 Er 𝑈)
6463adantr 276 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑅 Er 𝑈)
65 eropr.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴𝑈)
6665adantr 276 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐴𝑈)
67 simprll 537 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝐴)
6866, 67sseldd 3154 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝑈)
6964, 68erth 6569 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟𝑅𝑠 ↔ [𝑟]𝑅 = [𝑠]𝑅))
70 eropr.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Er 𝑉)
7170adantr 276 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑆 Er 𝑉)
72 eropr.8 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵𝑉)
7372adantr 276 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐵𝑉)
74 simprrl 539 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝐵)
7573, 74sseldd 3154 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝑉)
7671, 75erth 6569 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑡𝑆𝑢 ↔ [𝑡]𝑆 = [𝑢]𝑆))
7769, 76anbi12d 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
78 eropr.6 . . . . . . . . . . . . . . . 16 (𝜑𝑇 Er 𝑊)
7978adantr 276 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑇 Er 𝑊)
80 eropr.9 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝑊)
8180adantr 276 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐶𝑊)
82 eropr.10 . . . . . . . . . . . . . . . . . 18 (𝜑+ :(𝐴 × 𝐵)⟶𝐶)
8382adantr 276 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → + :(𝐴 × 𝐵)⟶𝐶)
8483, 67, 74fovcdmd 6009 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝐶)
8581, 84sseldd 3154 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝑊)
8679, 85erth 6569 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟 + 𝑡)𝑇(𝑠 + 𝑢) ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8762, 77, 863imtr3d 202 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
88 eqeq2 2185 . . . . . . . . . . . . . 14 (𝑤 = [(𝑠 + 𝑢)]𝑇 → ([(𝑟 + 𝑡)]𝑇 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8988biimprcd 160 . . . . . . . . . . . . 13 ([(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇 → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤))
9087, 89syl6 33 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
9190impd 254 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤))
92 eqeq1 2182 . . . . . . . . . . . . . . 15 (𝑋 = [𝑟]𝑅 → (𝑋 = [𝑠]𝑅 ↔ [𝑟]𝑅 = [𝑠]𝑅))
93 eqeq1 2182 . . . . . . . . . . . . . . 15 (𝑌 = [𝑡]𝑆 → (𝑌 = [𝑢]𝑆 ↔ [𝑡]𝑆 = [𝑢]𝑆))
9492, 93bi2anan9 606 . . . . . . . . . . . . . 14 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
9594anbi1d 465 . . . . . . . . . . . . 13 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
9695adantr 276 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
97 eqeq1 2182 . . . . . . . . . . . . 13 (𝑧 = [(𝑟 + 𝑡)]𝑇 → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9897adantl 277 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9996, 98imbi12d 234 . . . . . . . . . . 11 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → ((((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤) ↔ ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
10091, 99syl5ibrcom 157 . . . . . . . . . 10 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤)))
101100impd 254 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
102101anassrs 400 . . . . . . . 8 (((𝜑 ∧ (𝑟𝐴𝑠𝐴)) ∧ (𝑡𝐵𝑢𝐵)) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
103102rexlimdvva 2600 . . . . . . 7 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10461, 103syl5bir 153 . . . . . 6 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → ((∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
105104rexlimdvva 2600 . . . . 5 (𝜑 → (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10660, 105syl5bir 153 . . . 4 (𝜑 → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
107106adantr 276 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
108107alrimivv 1873 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
109 eqeq1 2182 . . . . 5 (𝑧 = 𝑤 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑝 + 𝑞)]𝑇))
110109anbi2d 464 . . . 4 (𝑧 = 𝑤 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
1111102rexbidv 2500 . . 3 (𝑧 = 𝑤 → (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
112111eu4 2086 . 2 (∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ (∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤)))
11327, 108, 112sylanbrc 417 1 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wal 1351   = wceq 1353  wex 1490  ∃!weu 2024  wcel 2146  wrex 2454  Vcvv 2735  wss 3127   class class class wbr 3998   × cxp 4618  wf 5204  (class class class)co 5865   Er wer 6522  [cec 6523   / cqs 6524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-v 2737  df-sbc 2961  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-opab 4060  df-id 4287  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-fv 5216  df-ov 5868  df-er 6525  df-ec 6527  df-qs 6531
This theorem is referenced by:  erovlem  6617  eroprf  6618
  Copyright terms: Public domain W3C validator