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

Theorem eroveu 6104
Description: Lemma for eroprf 6106. (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 6065 . . . . . . . 8 (𝑋 (A / 𝑅) → 𝑝 A 𝑋 = [𝑝]𝑅)
2 eropr.1 . . . . . . . 8 𝐽 = (A / 𝑅)
31, 2eleq2s 2110 . . . . . . 7 (𝑋 𝐽𝑝 A 𝑋 = [𝑝]𝑅)
4 elqsi 6065 . . . . . . . 8 (𝑌 (B / 𝑆) → 𝑞 B 𝑌 = [𝑞]𝑆)
5 eropr.2 . . . . . . . 8 𝐾 = (B / 𝑆)
64, 5eleq2s 2110 . . . . . . 7 (𝑌 𝐾𝑞 B 𝑌 = [𝑞]𝑆)
73, 6anim12i 321 . . . . . 6 ((𝑋 𝐽 𝑌 𝐾) → (𝑝 A 𝑋 = [𝑝]𝑅 𝑞 B 𝑌 = [𝑞]𝑆))
87adantl 262 . . . . 5 ((φ (𝑋 𝐽 𝑌 𝐾)) → (𝑝 A 𝑋 = [𝑝]𝑅 𝑞 B 𝑌 = [𝑞]𝑆))
9 reeanv 2453 . . . . 5 (𝑝 A 𝑞 B (𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑝 A 𝑋 = [𝑝]𝑅 𝑞 B 𝑌 = [𝑞]𝑆))
108, 9sylibr 137 . . . 4 ((φ (𝑋 𝐽 𝑌 𝐾)) → 𝑝 A 𝑞 B (𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆))
11 eropr.3 . . . . . . . 8 (φ𝑇 𝑍)
1211adantr 261 . . . . . . 7 ((φ (𝑋 𝐽 𝑌 𝐾)) → 𝑇 𝑍)
13 ecexg 6017 . . . . . . 7 (𝑇 𝑍 → [(𝑝 + 𝑞)]𝑇 V)
14 elisset 2541 . . . . . . 7 ([(𝑝 + 𝑞)]𝑇 V → z z = [(𝑝 + 𝑞)]𝑇)
1512, 13, 143syl 17 . . . . . 6 ((φ (𝑋 𝐽 𝑌 𝐾)) → z z = [(𝑝 + 𝑞)]𝑇)
1615biantrud 288 . . . . 5 ((φ (𝑋 𝐽 𝑌 𝐾)) → ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇)))
17162rexbidv 2323 . . . 4 ((φ (𝑋 𝐽 𝑌 𝐾)) → (𝑝 A 𝑞 B (𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇)))
1810, 17mpbid 135 . . 3 ((φ (𝑋 𝐽 𝑌 𝐾)) → 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇))
19 19.42v 1764 . . . . . . . 8 (z((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇))
2019bicomi 123 . . . . . . 7 (((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ z((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
2120rexbii 2305 . . . . . 6 (𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ 𝑞 B z((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
22 rexcom4 2550 . . . . . 6 (𝑞 B z((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ z𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
2321, 22bitri 173 . . . . 5 (𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ z𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
2423rexbii 2305 . . . 4 (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z z = [(𝑝 + 𝑞)]𝑇) ↔ 𝑝 A z𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
25 rexcom4 2550 . . . 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 2453 . . . . . 6 (𝑟 A 𝑠 A (𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) ↔ (𝑟 A 𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) 𝑠 A u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
29 eceq1 6048 . . . . . . . . . . 11 (𝑝 = 𝑟 → [𝑝]𝑅 = [𝑟]𝑅)
3029eqeq2d 2029 . . . . . . . . . 10 (𝑝 = 𝑟 → (𝑋 = [𝑝]𝑅𝑋 = [𝑟]𝑅))
3130anbi1d 441 . . . . . . . . 9 (𝑝 = 𝑟 → ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅 𝑌 = [𝑞]𝑆)))
32 oveq1 5439 . . . . . . . . . . 11 (𝑝 = 𝑟 → (𝑝 + 𝑞) = (𝑟 + 𝑞))
3332eceq1d 6049 . . . . . . . . . 10 (𝑝 = 𝑟 → [(𝑝 + 𝑞)]𝑇 = [(𝑟 + 𝑞)]𝑇)
3433eqeq2d 2029 . . . . . . . . 9 (𝑝 = 𝑟 → (z = [(𝑝 + 𝑞)]𝑇z = [(𝑟 + 𝑞)]𝑇))
3531, 34anbi12d 445 . . . . . . . 8 (𝑝 = 𝑟 → (((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑟 + 𝑞)]𝑇)))
36 eceq1 6048 . . . . . . . . . . 11 (𝑞 = 𝑡 → [𝑞]𝑆 = [𝑡]𝑆)
3736eqeq2d 2029 . . . . . . . . . 10 (𝑞 = 𝑡 → (𝑌 = [𝑞]𝑆𝑌 = [𝑡]𝑆))
3837anbi2d 440 . . . . . . . . 9 (𝑞 = 𝑡 → ((𝑋 = [𝑟]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆)))
39 oveq2 5440 . . . . . . . . . . 11 (𝑞 = 𝑡 → (𝑟 + 𝑞) = (𝑟 + 𝑡))
4039eceq1d 6049 . . . . . . . . . 10 (𝑞 = 𝑡 → [(𝑟 + 𝑞)]𝑇 = [(𝑟 + 𝑡)]𝑇)
4140eqeq2d 2029 . . . . . . . . 9 (𝑞 = 𝑡 → (z = [(𝑟 + 𝑞)]𝑇z = [(𝑟 + 𝑡)]𝑇))
4238, 41anbi12d 445 . . . . . . . 8 (𝑞 = 𝑡 → (((𝑋 = [𝑟]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑟 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇)))
4335, 42cbvrex2v 2516 . . . . . . 7 (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ 𝑟 A 𝑡 B ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇))
44 eceq1 6048 . . . . . . . . . . 11 (𝑝 = 𝑠 → [𝑝]𝑅 = [𝑠]𝑅)
4544eqeq2d 2029 . . . . . . . . . 10 (𝑝 = 𝑠 → (𝑋 = [𝑝]𝑅𝑋 = [𝑠]𝑅))
4645anbi1d 441 . . . . . . . . 9 (𝑝 = 𝑠 → ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅 𝑌 = [𝑞]𝑆)))
47 oveq1 5439 . . . . . . . . . . 11 (𝑝 = 𝑠 → (𝑝 + 𝑞) = (𝑠 + 𝑞))
4847eceq1d 6049 . . . . . . . . . 10 (𝑝 = 𝑠 → [(𝑝 + 𝑞)]𝑇 = [(𝑠 + 𝑞)]𝑇)
4948eqeq2d 2029 . . . . . . . . 9 (𝑝 = 𝑠 → (w = [(𝑝 + 𝑞)]𝑇w = [(𝑠 + 𝑞)]𝑇))
5046, 49anbi12d 445 . . . . . . . 8 (𝑝 = 𝑠 → (((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑠 + 𝑞)]𝑇)))
51 eceq1 6048 . . . . . . . . . . 11 (𝑞 = u → [𝑞]𝑆 = [u]𝑆)
5251eqeq2d 2029 . . . . . . . . . 10 (𝑞 = u → (𝑌 = [𝑞]𝑆𝑌 = [u]𝑆))
5352anbi2d 440 . . . . . . . . 9 (𝑞 = u → ((𝑋 = [𝑠]𝑅 𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆)))
54 oveq2 5440 . . . . . . . . . . 11 (𝑞 = u → (𝑠 + 𝑞) = (𝑠 + u))
5554eceq1d 6049 . . . . . . . . . 10 (𝑞 = u → [(𝑠 + 𝑞)]𝑇 = [(𝑠 + u)]𝑇)
5655eqeq2d 2029 . . . . . . . . 9 (𝑞 = u → (w = [(𝑠 + 𝑞)]𝑇w = [(𝑠 + u)]𝑇))
5753, 56anbi12d 445 . . . . . . . 8 (𝑞 = u → (((𝑋 = [𝑠]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑠 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
5850, 57cbvrex2v 2516 . . . . . . 7 (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇) ↔ 𝑠 A u B ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇))
5943, 58anbi12i 436 . . . . . 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 2453 . . . . . . 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 477 . . . . . . . . . . . . . . . . 17 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑟 A)
6866, 67sseldd 2919 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑟 𝑈)
6964, 68erth 6057 . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . 17 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑡 B)
7573, 74sseldd 2919 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → 𝑡 𝑉)
7671, 75erth 6057 . . . . . . . . . . . . . . 15 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (𝑡𝑆u ↔ [𝑡]𝑆 = [u]𝑆))
7769, 76anbi12d 445 . . . . . . . . . . . . . 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 5564 . . . . . . . . . . . . . . . 16 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (𝑟 + 𝑡) 𝐶)
8581, 84sseldd 2919 . . . . . . . . . . . . . . 15 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (𝑟 + 𝑡) 𝑊)
8679, 85erth 6057 . . . . . . . . . . . . . 14 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((𝑟 + 𝑡)𝑇(𝑠 + u) ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + u)]𝑇))
8762, 77, 863imtr3d 191 . . . . . . . . . . . . 13 ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → (([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) → [(𝑟 + 𝑡)]𝑇 = [(𝑠 + u)]𝑇))
88 eqeq2 2027 . . . . . . . . . . . . . 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 2024 . . . . . . . . . . . . . . 15 (𝑋 = [𝑟]𝑅 → (𝑋 = [𝑠]𝑅 ↔ [𝑟]𝑅 = [𝑠]𝑅))
93 eqeq1 2024 . . . . . . . . . . . . . . 15 (𝑌 = [𝑡]𝑆 → (𝑌 = [u]𝑆 ↔ [𝑡]𝑆 = [u]𝑆))
9492, 93bi2anan9 526 . . . . . . . . . . . . . 14 ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) → ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) ↔ ([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆)))
9594anbi1d 441 . . . . . . . . . . . . 13 ((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) → (((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
9695adantr 261 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 [𝑡]𝑆 = [u]𝑆) w = [(𝑠 + u)]𝑇)))
97 eqeq1 2024 . . . . . . . . . . . . 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 382 . . . . . . . 8 (((φ (𝑟 A 𝑠 A)) (𝑡 B u B)) → ((((𝑋 = [𝑟]𝑅 𝑌 = [𝑡]𝑆) z = [(𝑟 + 𝑡)]𝑇) ((𝑋 = [𝑠]𝑅 𝑌 = [u]𝑆) w = [(𝑠 + u)]𝑇)) → z = w))
103102rexlimdvva 2414 . . . . . . 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 2414 . . . . 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 1733 . 2 ((φ (𝑋 𝐽 𝑌 𝐾)) → zw((𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)) → z = w))
109 eqeq1 2024 . . . . 5 (z = w → (z = [(𝑝 + 𝑞)]𝑇w = [(𝑝 + 𝑞)]𝑇))
110109anbi2d 440 . . . 4 (z = w → (((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)))
1111102rexbidv 2323 . . 3 (z = w → (𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)))
112111eu4 1940 . 2 (∃!z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) ↔ (z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) zw((𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇) 𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) w = [(𝑝 + 𝑞)]𝑇)) → z = w)))
11327, 108, 112sylanbrc 396 1 ((φ (𝑋 𝐽 𝑌 𝐾)) → ∃!z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  wal 1224   = wceq 1226  wex 1358   wcel 1370  ∃!weu 1878  wrex 2281  Vcvv 2531  wss 2890   class class class wbr 3734   × cxp 4266  wf 4821  (class class class)co 5432   Er wer 6010  [cec 6011   / cqs 6012
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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-un 4116
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-fv 4833  df-ov 5435  df-er 6013  df-ec 6015  df-qs 6019
This theorem is referenced by:  erovlem  6105  eroprf  6106
  Copyright terms: Public domain W3C validator