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

Theorem eroveu 6133
Description: Lemma for eroprf 6135. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
Hypotheses
Ref Expression
eropr.1 𝐽 = (A / 𝑅)
eropr.2 𝐾 = (B / 𝑆)
eropr.3 (φ𝑇 𝑍)
eropr.4 (φ𝑅 Er 𝑈)
eropr.5 (φ𝑆 Er 𝑉)
eropr.6 (φ𝑇 Er 𝑊)
eropr.7 (φA𝑈)
eropr.8 (φB𝑉)
eropr.9 (φ𝐶𝑊)
eropr.10 (φ+ :(A × B)⟶𝐶)
eropr.11 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((𝑟𝑅𝑠 𝑡𝑆u) → (𝑟 + 𝑡)𝑇(𝑠 + u)))
Assertion
Ref Expression
eroveu ((φ (𝑋 𝐽 𝑌 𝐾)) → ∃!z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
Distinct variable groups:   𝑞,𝑝,𝑟,𝑠,𝑡,u,z,A   B,𝑝,𝑞,𝑟,𝑠,𝑡,u,z   𝐽,𝑝,𝑞,z   𝑅,𝑝,𝑞,𝑟,𝑠,𝑡,u,z   𝐾,𝑝,𝑞,z   𝑆,𝑝,𝑞,𝑟,𝑠,𝑡,u,z   + ,𝑝,𝑞,𝑟,𝑠,𝑡,u,z   φ,𝑝,𝑞,𝑟,𝑠,𝑡,u,z   𝑇,𝑝,𝑞,𝑟,𝑠,𝑡,u,z   𝑋,𝑝,𝑞,𝑟,𝑠,𝑡,u,z   𝑌,𝑝,𝑞,𝑟,𝑠,𝑡,u,z
Allowed substitution hints:   𝐶(z,u,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑈(z,u,𝑡,𝑠,𝑟,𝑞,𝑝)   𝐽(u,𝑡,𝑠,𝑟)   𝐾(u,𝑡,𝑠,𝑟)   𝑉(z,u,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑊(z,u,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑍(z,u,𝑡,𝑠,𝑟,𝑞,𝑝)

Proof of Theorem eroveu
Dummy variable w is distinct from all other variables.
StepHypRef Expression
1 elqsi 6094 . . . . . . . 8 (𝑋 (A / 𝑅) → 𝑝 A 𝑋 = [𝑝]𝑅)
2 eropr.1 . . . . . . . 8 𝐽 = (A / 𝑅)
31, 2eleq2s 2129 . . . . . . 7 (𝑋 𝐽𝑝 A 𝑋 = [𝑝]𝑅)
4 elqsi 6094 . . . . . . . 8 (𝑌 (B / 𝑆) → 𝑞 B 𝑌 = [𝑞]𝑆)
5 eropr.2 . . . . . . . 8 𝐾 = (B / 𝑆)
64, 5eleq2s 2129 . . . . . . 7 (𝑌 𝐾𝑞 B 𝑌 = [𝑞]𝑆)
73, 6anim12i 321 . . . . . 6 ((𝑋 𝐽 𝑌 𝐾) → (𝑝 A 𝑋 = [𝑝]𝑅 𝑞 B 𝑌 = [𝑞]𝑆))
87adantl 262 . . . . 5 ((φ (𝑋 𝐽 𝑌 𝐾)) → (𝑝 A 𝑋 = [𝑝]𝑅 𝑞 B 𝑌 = [𝑞]𝑆))
9 reeanv 2473 . . . . 5 (𝑝 A 𝑞 B (𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑝 A 𝑋 = [𝑝]𝑅 𝑞 B 𝑌 = [𝑞]𝑆))
108, 9sylibr 137 . . . 4 ((φ (𝑋 𝐽 𝑌 𝐾)) → 𝑝 A 𝑞 B (𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆))
11 eropr.3 . . . . . . . 8 (φ𝑇 𝑍)
1211adantr 261 . . . . . . 7 ((φ (𝑋 𝐽 𝑌 𝐾)) → 𝑇 𝑍)
13 ecexg 6046 . . . . . . 7 (𝑇 𝑍 → [(𝑝 + 𝑞)]𝑇 V)
14 elisset 2562 . . . . . . 7 ([(𝑝 + 𝑞)]𝑇 V → z z = [(𝑝 + 𝑞)]𝑇)
1512, 13, 143syl 17 . . . . . 6 ((φ (𝑋 𝐽 𝑌 𝐾)) → z z = [(𝑝 + 𝑞)]𝑇)
1615biantrud 288 . . . . 5 ((φ (𝑋 𝐽 𝑌 𝐾)) → ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇)))
17162rexbidv 2343 . . . 4 ((φ (𝑋 𝐽 𝑌 𝐾)) → (𝑝 A 𝑞 B (𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇)))
1810, 17mpbid 135 . . 3 ((φ (𝑋 𝐽 𝑌 𝐾)) → 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇))
19 19.42v 1783 . . . . . . . 8 (z((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇))
2019bicomi 123 . . . . . . 7 (((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ z((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
2120rexbii 2325 . . . . . 6 (𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ 𝑞 B z((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
22 rexcom4 2571 . . . . . 6 (𝑞 B z((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ z𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
2321, 22bitri 173 . . . . 5 (𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ z𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
2423rexbii 2325 . . . 4 (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ 𝑝 A z𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
25 rexcom4 2571 . . . 4 (𝑝 A z𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
2624, 25bitri 173 . . 3 (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
2718, 26sylib 127 . 2 ((φ (𝑋 𝐽 𝑌 𝐾)) → z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
28 reeanv 2473 . . . . . 6 (𝑟 A 𝑠 A (𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) ↔ (𝑟 A 𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) 𝑠 A u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
29 eceq1 6077 . . . . . . . . . . 11 (𝑝 = 𝑟 → [𝑝]𝑅 = [𝑟]𝑅)
3029eqeq2d 2048 . . . . . . . . . 10 (𝑝 = 𝑟 → (𝑋 = [𝑝]𝑅𝑋 = [𝑟]𝑅))
3130anbi1d 438 . . . . . . . . 9 (𝑝 = 𝑟 → ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅 𝑌 = [𝑞]𝑆)))
32 oveq1 5462 . . . . . . . . . . 11 (𝑝 = 𝑟 → (𝑝 + 𝑞) = (𝑟 + 𝑞))
3332eceq1d 6078 . . . . . . . . . 10 (𝑝 = 𝑟 → [(𝑝 + 𝑞)]𝑇 = [(𝑟 + 𝑞)]𝑇)
3433eqeq2d 2048 . . . . . . . . 9 (𝑝 = 𝑟 → (z = [(𝑝 + 𝑞)]𝑇z = [(𝑟 + 𝑞)]𝑇))
3531, 34anbi12d 442 . . . . . . . 8 (𝑝 = 𝑟 → (((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑟 + 𝑞)]𝑇)))
36 eceq1 6077 . . . . . . . . . . 11 (𝑞 = 𝑡 → [𝑞]𝑆 = [𝑡]𝑆)
3736eqeq2d 2048 . . . . . . . . . 10 (𝑞 = 𝑡 → (𝑌 = [𝑞]𝑆𝑌 = [𝑡]𝑆))
3837anbi2d 437 . . . . . . . . 9 (𝑞 = 𝑡 → ((𝑋 = [𝑟]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆)))
39 oveq2 5463 . . . . . . . . . . 11 (𝑞 = 𝑡 → (𝑟 + 𝑞) = (𝑟 + 𝑡))
4039eceq1d 6078 . . . . . . . . . 10 (𝑞 = 𝑡 → [(𝑟 + 𝑞)]𝑇 = [(𝑟 + 𝑡)]𝑇)
4140eqeq2d 2048 . . . . . . . . 9 (𝑞 = 𝑡 → (z = [(𝑟 + 𝑞)]𝑇z = [(𝑟 + 𝑡)]𝑇))
4238, 41anbi12d 442 . . . . . . . 8 (𝑞 = 𝑡 → (((𝑋 = [𝑟]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑟 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇)))
4335, 42cbvrex2v 2536 . . . . . . 7 (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ 𝑟 A 𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇))
44 eceq1 6077 . . . . . . . . . . 11 (𝑝 = 𝑠 → [𝑝]𝑅 = [𝑠]𝑅)
4544eqeq2d 2048 . . . . . . . . . 10 (𝑝 = 𝑠 → (𝑋 = [𝑝]𝑅𝑋 = [𝑠]𝑅))
4645anbi1d 438 . . . . . . . . 9 (𝑝 = 𝑠 → ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅 𝑌 = [𝑞]𝑆)))
47 oveq1 5462 . . . . . . . . . . 11 (𝑝 = 𝑠 → (𝑝 + 𝑞) = (𝑠 + 𝑞))
4847eceq1d 6078 . . . . . . . . . 10 (𝑝 = 𝑠 → [(𝑝 + 𝑞)]𝑇 = [(𝑠 + 𝑞)]𝑇)
4948eqeq2d 2048 . . . . . . . . 9 (𝑝 = 𝑠 → (w = [(𝑝 + 𝑞)]𝑇w = [(𝑠 + 𝑞)]𝑇))
5046, 49anbi12d 442 . . . . . . . 8 (𝑝 = 𝑠 → (((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑠 + 𝑞)]𝑇)))
51 eceq1 6077 . . . . . . . . . . 11 (𝑞 = u → [𝑞]𝑆 = [u]𝑆)
5251eqeq2d 2048 . . . . . . . . . 10 (𝑞 = u → (𝑌 = [𝑞]𝑆𝑌 = [u]𝑆))
5352anbi2d 437 . . . . . . . . 9 (𝑞 = u → ((𝑋 = [𝑠]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆)))
54 oveq2 5463 . . . . . . . . . . 11 (𝑞 = u → (𝑠 + 𝑞) = (𝑠 + u))
5554eceq1d 6078 . . . . . . . . . 10 (𝑞 = u → [(𝑠 + 𝑞)]𝑇 = [(𝑠 + u)]𝑇)
5655eqeq2d 2048 . . . . . . . . 9 (𝑞 = u → (w = [(𝑠 + 𝑞)]𝑇w = [(𝑠 + u)]𝑇))
5753, 56anbi12d 442 . . . . . . . 8 (𝑞 = u → (((𝑋 = [𝑠]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑠 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
5850, 57cbvrex2v 2536 . . . . . . 7 (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇) ↔ 𝑠 A u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇))
5943, 58anbi12i 433 . . . . . 6 ((𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)) ↔ (𝑟 A 𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) 𝑠 A u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
6028, 59bitr4i 176 . . . . 5 (𝑟 A 𝑠 A (𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) ↔ (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)))
61 reeanv 2473 . . . . . . 7 (𝑡 B u B (((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) ↔ (𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
62 eropr.11 . . . . . . . . . . . . . 14 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((𝑟𝑅𝑠 𝑡𝑆u) → (𝑟 + 𝑡)𝑇(𝑠 + u)))
63 eropr.4 . . . . . . . . . . . . . . . . 17 (φ𝑅 Er 𝑈)
6463adantr 261 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑅 Er 𝑈)
65 eropr.7 . . . . . . . . . . . . . . . . . 18 (φA𝑈)
6665adantr 261 . . . . . . . . . . . . . . . . 17 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → A𝑈)
67 simprll 489 . . . . . . . . . . . . . . . . 17 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑟 A)
6866, 67sseldd 2940 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑟 𝑈)
6964, 68erth 6086 . . . . . . . . . . . . . . 15 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (𝑟𝑅𝑠 ↔ [𝑟]𝑅 = [𝑠]𝑅))
70 eropr.5 . . . . . . . . . . . . . . . . 17 (φ𝑆 Er 𝑉)
7170adantr 261 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑆 Er 𝑉)
72 eropr.8 . . . . . . . . . . . . . . . . . 18 (φB𝑉)
7372adantr 261 . . . . . . . . . . . . . . . . 17 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → B𝑉)
74 simprrl 491 . . . . . . . . . . . . . . . . 17 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑡 B)
7573, 74sseldd 2940 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑡 𝑉)
7671, 75erth 6086 . . . . . . . . . . . . . . 15 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (𝑡𝑆u ↔ [𝑡]𝑆 = [u]𝑆))
7769, 76anbi12d 442 . . . . . . . . . . . . . 14 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((𝑟𝑅𝑠 𝑡𝑆u) ↔ ([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆)))
78 eropr.6 . . . . . . . . . . . . . . . 16 (φ𝑇 Er 𝑊)
7978adantr 261 . . . . . . . . . . . . . . 15 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑇 Er 𝑊)
80 eropr.9 . . . . . . . . . . . . . . . . 17 (φ𝐶𝑊)
8180adantr 261 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝐶𝑊)
82 eropr.10 . . . . . . . . . . . . . . . . . 18 (φ+ :(A × B)⟶𝐶)
8382adantr 261 . . . . . . . . . . . . . . . . 17 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → + :(A × B)⟶𝐶)
8483, 67, 74fovrnd 5587 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (𝑟 + 𝑡) 𝐶)
8581, 84sseldd 2940 . . . . . . . . . . . . . . 15 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (𝑟 + 𝑡) 𝑊)
8679, 85erth 6086 . . . . . . . . . . . . . 14 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((𝑟 + 𝑡)𝑇(𝑠 + u) ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + u)]𝑇))
8762, 77, 863imtr3d 191 . . . . . . . . . . . . 13 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) → [(𝑟 + 𝑡)]𝑇 = [(𝑠 + u)]𝑇))
88 eqeq2 2046 . . . . . . . . . . . . . 14 (w = [(𝑠 + u)]𝑇 → ([(𝑟 + 𝑡)]𝑇 = w ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + u)]𝑇))
8988biimprcd 149 . . . . . . . . . . . . 13 ([(𝑟 + 𝑡)]𝑇 = [(𝑠 + u)]𝑇 → (w = [(𝑠 + u)]𝑇 → [(𝑟 + 𝑡)]𝑇 = w))
9087, 89syl6 29 . . . . . . . . . . . 12 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) → (w = [(𝑠 + u)]𝑇 → [(𝑟 + 𝑡)]𝑇 = w)))
9190impd 242 . . . . . . . . . . 11 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) w = [(𝑠 + u)]𝑇) → [(𝑟 + 𝑡)]𝑇 = w))
92 eqeq1 2043 . . . . . . . . . . . . . . 15 (𝑋 = [𝑟]𝑅 → (𝑋 = [𝑠]𝑅 ↔ [𝑟]𝑅 = [𝑠]𝑅))
93 eqeq1 2043 . . . . . . . . . . . . . . 15 (𝑌 = [𝑡]𝑆 → (𝑌 = [u]𝑆 ↔ [𝑡]𝑆 = [u]𝑆))
9492, 93bi2anan9 538 . . . . . . . . . . . . . 14 ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) → ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) ↔ ([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆)))
9594anbi1d 438 . . . . . . . . . . . . 13 ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) → (((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
9695adantr 261 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
97 eqeq1 2043 . . . . . . . . . . . . 13 (z = [(𝑟 + 𝑡)]𝑇 → (z = w ↔ [(𝑟 + 𝑡)]𝑇 = w))
9897adantl 262 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) → (z = w ↔ [(𝑟 + 𝑡)]𝑇 = w))
9996, 98imbi12d 223 . . . . . . . . . . 11 (((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) → ((((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇) → z = w) ↔ ((([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) w = [(𝑠 + u)]𝑇) → [(𝑟 + 𝑡)]𝑇 = w)))
10091, 99syl5ibrcom 146 . . . . . . . . . 10 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇) → z = w)))
101100impd 242 . . . . . . . . 9 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) → z = w))
102101anassrs 380 . . . . . . . 8 (((φ (𝑟 A 𝑠 A)) (𝑡 B u B)) → ((((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) → z = w))
103102rexlimdvva 2434 . . . . . . 7 ((φ (𝑟 A 𝑠 A)) → (𝑡 B u B (((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) → z = w))
10461, 103syl5bir 142 . . . . . 6 ((φ (𝑟 A 𝑠 A)) → ((𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) → z = w))
105104rexlimdvva 2434 . . . . 5 (φ → (𝑟 A 𝑠 A (𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) → z = w))
10660, 105syl5bir 142 . . . 4 (φ → ((𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)) → z = w))
107106adantr 261 . . 3 ((φ (𝑋 𝐽 𝑌 𝐾)) → ((𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)) → z = w))
108107alrimivv 1752 . 2 ((φ (𝑋 𝐽 𝑌 𝐾)) → zw((𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)) → z = w))
109 eqeq1 2043 . . . . 5 (z = w → (z = [(𝑝 + 𝑞)]𝑇w = [(𝑝 + 𝑞)]𝑇))
110109anbi2d 437 . . . 4 (z = w → (((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)))
1111102rexbidv 2343 . . 3 (z = w → (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)))
112111eu4 1959 . 2 (∃!z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ (z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) zw((𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)) → z = w)))
11327, 108, 112sylanbrc 394 1 ((φ (𝑋 𝐽 𝑌 𝐾)) → ∃!z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  wal 1240   = wceq 1242  wex 1378   wcel 1390  ∃!weu 1897  wrex 2301  Vcvv 2551  wss 2911   class class class wbr 3755   × cxp 4286  wf 4841  (class class class)co 5455   Er wer 6039  [cec 6040   / cqs 6041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-fv 4853  df-ov 5458  df-er 6042  df-ec 6044  df-qs 6048
This theorem is referenced by:  erovlem  6134  eroprf  6135
  Copyright terms: Public domain W3C validator