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

Theorem eroveu 6227
Description: Lemma for eroprf 6229. (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 6188 . . . . . . . 8 (𝑋 ∈ (𝐴 / 𝑅) → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
2 eropr.1 . . . . . . . 8 𝐽 = (𝐴 / 𝑅)
31, 2eleq2s 2148 . . . . . . 7 (𝑋𝐽 → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
4 elqsi 6188 . . . . . . . 8 (𝑌 ∈ (𝐵 / 𝑆) → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
5 eropr.2 . . . . . . . 8 𝐾 = (𝐵 / 𝑆)
64, 5eleq2s 2148 . . . . . . 7 (𝑌𝐾 → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
73, 6anim12i 325 . . . . . 6 ((𝑋𝐽𝑌𝐾) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
87adantl 266 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
9 reeanv 2496 . . . . 5 (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
108, 9sylibr 141 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆))
11 eropr.3 . . . . . . . 8 (𝜑𝑇𝑍)
1211adantr 265 . . . . . . 7 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → 𝑇𝑍)
13 ecexg 6140 . . . . . . 7 (𝑇𝑍 → [(𝑝 + 𝑞)]𝑇 ∈ V)
14 elisset 2585 . . . . . . 7 ([(𝑝 + 𝑞)]𝑇 ∈ V → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1512, 13, 143syl 17 . . . . . 6 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1615biantrud 292 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
17162rexbidv 2366 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
1810, 17mpbid 139 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
19 19.42v 1802 . . . . . . . 8 (∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
2019bicomi 127 . . . . . . 7 (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2120rexbii 2348 . . . . . 6 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
22 rexcom4 2594 . . . . . 6 (∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2321, 22bitri 177 . . . . 5 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2423rexbii 2348 . . . 4 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
25 rexcom4 2594 . . . 4 (∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2624, 25bitri 177 . . 3 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2718, 26sylib 131 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
28 reeanv 2496 . . . . . 6 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
29 eceq1 6171 . . . . . . . . . . 11 (𝑝 = 𝑟 → [𝑝]𝑅 = [𝑟]𝑅)
3029eqeq2d 2067 . . . . . . . . . 10 (𝑝 = 𝑟 → (𝑋 = [𝑝]𝑅𝑋 = [𝑟]𝑅))
3130anbi1d 446 . . . . . . . . 9 (𝑝 = 𝑟 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆)))
32 oveq1 5546 . . . . . . . . . . 11 (𝑝 = 𝑟 → (𝑝 + 𝑞) = (𝑟 + 𝑞))
3332eceq1d 6172 . . . . . . . . . 10 (𝑝 = 𝑟 → [(𝑝 + 𝑞)]𝑇 = [(𝑟 + 𝑞)]𝑇)
3433eqeq2d 2067 . . . . . . . . 9 (𝑝 = 𝑟 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑞)]𝑇))
3531, 34anbi12d 450 . . . . . . . 8 (𝑝 = 𝑟 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇)))
36 eceq1 6171 . . . . . . . . . . 11 (𝑞 = 𝑡 → [𝑞]𝑆 = [𝑡]𝑆)
3736eqeq2d 2067 . . . . . . . . . 10 (𝑞 = 𝑡 → (𝑌 = [𝑞]𝑆𝑌 = [𝑡]𝑆))
3837anbi2d 445 . . . . . . . . 9 (𝑞 = 𝑡 → ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆)))
39 oveq2 5547 . . . . . . . . . . 11 (𝑞 = 𝑡 → (𝑟 + 𝑞) = (𝑟 + 𝑡))
4039eceq1d 6172 . . . . . . . . . 10 (𝑞 = 𝑡 → [(𝑟 + 𝑞)]𝑇 = [(𝑟 + 𝑡)]𝑇)
4140eqeq2d 2067 . . . . . . . . 9 (𝑞 = 𝑡 → (𝑧 = [(𝑟 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑡)]𝑇))
4238, 41anbi12d 450 . . . . . . . 8 (𝑞 = 𝑡 → (((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇)))
4335, 42cbvrex2v 2559 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇))
44 eceq1 6171 . . . . . . . . . . 11 (𝑝 = 𝑠 → [𝑝]𝑅 = [𝑠]𝑅)
4544eqeq2d 2067 . . . . . . . . . 10 (𝑝 = 𝑠 → (𝑋 = [𝑝]𝑅𝑋 = [𝑠]𝑅))
4645anbi1d 446 . . . . . . . . 9 (𝑝 = 𝑠 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆)))
47 oveq1 5546 . . . . . . . . . . 11 (𝑝 = 𝑠 → (𝑝 + 𝑞) = (𝑠 + 𝑞))
4847eceq1d 6172 . . . . . . . . . 10 (𝑝 = 𝑠 → [(𝑝 + 𝑞)]𝑇 = [(𝑠 + 𝑞)]𝑇)
4948eqeq2d 2067 . . . . . . . . 9 (𝑝 = 𝑠 → (𝑤 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑞)]𝑇))
5046, 49anbi12d 450 . . . . . . . 8 (𝑝 = 𝑠 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇)))
51 eceq1 6171 . . . . . . . . . . 11 (𝑞 = 𝑢 → [𝑞]𝑆 = [𝑢]𝑆)
5251eqeq2d 2067 . . . . . . . . . 10 (𝑞 = 𝑢 → (𝑌 = [𝑞]𝑆𝑌 = [𝑢]𝑆))
5352anbi2d 445 . . . . . . . . 9 (𝑞 = 𝑢 → ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆)))
54 oveq2 5547 . . . . . . . . . . 11 (𝑞 = 𝑢 → (𝑠 + 𝑞) = (𝑠 + 𝑢))
5554eceq1d 6172 . . . . . . . . . 10 (𝑞 = 𝑢 → [(𝑠 + 𝑞)]𝑇 = [(𝑠 + 𝑢)]𝑇)
5655eqeq2d 2067 . . . . . . . . 9 (𝑞 = 𝑢 → (𝑤 = [(𝑠 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑢)]𝑇))
5753, 56anbi12d 450 . . . . . . . 8 (𝑞 = 𝑢 → (((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
5850, 57cbvrex2v 2559 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))
5943, 58anbi12i 441 . . . . . 6 ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
6028, 59bitr4i 180 . . . . 5 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
61 reeanv 2496 . . . . . . 7 (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
62 eropr.11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))
63 eropr.4 . . . . . . . . . . . . . . . . 17 (𝜑𝑅 Er 𝑈)
6463adantr 265 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑅 Er 𝑈)
65 eropr.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴𝑈)
6665adantr 265 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐴𝑈)
67 simprll 497 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝐴)
6866, 67sseldd 2973 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝑈)
6964, 68erth 6180 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟𝑅𝑠 ↔ [𝑟]𝑅 = [𝑠]𝑅))
70 eropr.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Er 𝑉)
7170adantr 265 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑆 Er 𝑉)
72 eropr.8 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵𝑉)
7372adantr 265 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐵𝑉)
74 simprrl 499 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝐵)
7573, 74sseldd 2973 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝑉)
7671, 75erth 6180 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑡𝑆𝑢 ↔ [𝑡]𝑆 = [𝑢]𝑆))
7769, 76anbi12d 450 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
78 eropr.6 . . . . . . . . . . . . . . . 16 (𝜑𝑇 Er 𝑊)
7978adantr 265 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑇 Er 𝑊)
80 eropr.9 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝑊)
8180adantr 265 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐶𝑊)
82 eropr.10 . . . . . . . . . . . . . . . . . 18 (𝜑+ :(𝐴 × 𝐵)⟶𝐶)
8382adantr 265 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → + :(𝐴 × 𝐵)⟶𝐶)
8483, 67, 74fovrnd 5672 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝐶)
8581, 84sseldd 2973 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝑊)
8679, 85erth 6180 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟 + 𝑡)𝑇(𝑠 + 𝑢) ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8762, 77, 863imtr3d 195 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
88 eqeq2 2065 . . . . . . . . . . . . . 14 (𝑤 = [(𝑠 + 𝑢)]𝑇 → ([(𝑟 + 𝑡)]𝑇 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8988biimprcd 153 . . . . . . . . . . . . 13 ([(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇 → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤))
9087, 89syl6 33 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
9190impd 246 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤))
92 eqeq1 2062 . . . . . . . . . . . . . . 15 (𝑋 = [𝑟]𝑅 → (𝑋 = [𝑠]𝑅 ↔ [𝑟]𝑅 = [𝑠]𝑅))
93 eqeq1 2062 . . . . . . . . . . . . . . 15 (𝑌 = [𝑡]𝑆 → (𝑌 = [𝑢]𝑆 ↔ [𝑡]𝑆 = [𝑢]𝑆))
9492, 93bi2anan9 548 . . . . . . . . . . . . . 14 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
9594anbi1d 446 . . . . . . . . . . . . 13 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
9695adantr 265 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
97 eqeq1 2062 . . . . . . . . . . . . 13 (𝑧 = [(𝑟 + 𝑡)]𝑇 → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9897adantl 266 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9996, 98imbi12d 227 . . . . . . . . . . 11 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → ((((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤) ↔ ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
10091, 99syl5ibrcom 150 . . . . . . . . . 10 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤)))
101100impd 246 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
102101anassrs 386 . . . . . . . 8 (((𝜑 ∧ (𝑟𝐴𝑠𝐴)) ∧ (𝑡𝐵𝑢𝐵)) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
103102rexlimdvva 2457 . . . . . . 7 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10461, 103syl5bir 146 . . . . . 6 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → ((∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
105104rexlimdvva 2457 . . . . 5 (𝜑 → (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10660, 105syl5bir 146 . . . 4 (𝜑 → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
107106adantr 265 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
108107alrimivv 1771 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
109 eqeq1 2062 . . . . 5 (𝑧 = 𝑤 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑝 + 𝑞)]𝑇))
110109anbi2d 445 . . . 4 (𝑧 = 𝑤 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
1111102rexbidv 2366 . . 3 (𝑧 = 𝑤 → (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
112111eu4 1978 . 2 (∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ (∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤)))
11327, 108, 112sylanbrc 402 1 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102  wal 1257   = wceq 1259  wex 1397  wcel 1409  ∃!weu 1916  wrex 2324  Vcvv 2574  wss 2944   class class class wbr 3791   × cxp 4370  wf 4925  (class class class)co 5539   Er wer 6133  [cec 6134   / cqs 6135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-un 4197
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-sbc 2787  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-id 4057  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-fv 4937  df-ov 5542  df-er 6136  df-ec 6138  df-qs 6142
This theorem is referenced by:  erovlem  6228  eroprf  6229
  Copyright terms: Public domain W3C validator