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

Theorem addcanprleml 6770
Description: Lemma for addcanprg 6772. (Contributed by Jim Kingdon, 25-Dec-2019.)
Assertion
Ref Expression
addcanprleml (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (1st𝐵) ⊆ (1st𝐶))

Proof of Theorem addcanprleml
Dummy variables 𝑓 𝑔 𝑟 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prop 6631 . . . . . . 7 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
2 prnmaddl 6646 . . . . . . 7 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
31, 2sylan 271 . . . . . 6 ((𝐵P𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
433ad2antl2 1078 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ 𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
54adantlr 454 . . . 4 ((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
6 simprl 491 . . . . . 6 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑤Q)
7 halfnqq 6566 . . . . . 6 (𝑤Q → ∃𝑡Q (𝑡 +Q 𝑡) = 𝑤)
86, 7syl 14 . . . . 5 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → ∃𝑡Q (𝑡 +Q 𝑡) = 𝑤)
9 simplll 493 . . . . . . . . . 10 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → (𝐴P𝐵P𝐶P))
109adantr 265 . . . . . . . . 9 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝐴P𝐵P𝐶P))
1110simp1d 927 . . . . . . . 8 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝐴P)
12 prop 6631 . . . . . . . 8 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
1311, 12syl 14 . . . . . . 7 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
14 simprl 491 . . . . . . 7 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑡Q)
15 prarloc2 6660 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑡Q) → ∃𝑢 ∈ (1st𝐴)(𝑢 +Q 𝑡) ∈ (2nd𝐴))
1613, 14, 15syl2anc 397 . . . . . 6 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → ∃𝑢 ∈ (1st𝐴)(𝑢 +Q 𝑡) ∈ (2nd𝐴))
179ad2antrr 465 . . . . . . . . . . . 12 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝐴P𝐵P𝐶P))
1817simp1d 927 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐴P)
1917simp2d 928 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐵P)
20 addclpr 6693 . . . . . . . . . . 11 ((𝐴P𝐵P) → (𝐴 +P 𝐵) ∈ P)
2118, 19, 20syl2anc 397 . . . . . . . . . 10 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝐴 +P 𝐵) ∈ P)
22 prop 6631 . . . . . . . . . 10 ((𝐴 +P 𝐵) ∈ P → ⟨(1st ‘(𝐴 +P 𝐵)), (2nd ‘(𝐴 +P 𝐵))⟩ ∈ P)
2321, 22syl 14 . . . . . . . . 9 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ⟨(1st ‘(𝐴 +P 𝐵)), (2nd ‘(𝐴 +P 𝐵))⟩ ∈ P)
2418, 12syl 14 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
25 simprl 491 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑢 ∈ (1st𝐴))
26 elprnql 6637 . . . . . . . . . . 11 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑢 ∈ (1st𝐴)) → 𝑢Q)
2724, 25, 26syl2anc 397 . . . . . . . . . 10 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑢Q)
2819, 1syl 14 . . . . . . . . . . . 12 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
29 simplr 490 . . . . . . . . . . . . 13 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑣 ∈ (1st𝐵))
3029ad2antrr 465 . . . . . . . . . . . 12 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 ∈ (1st𝐵))
31 elprnql 6637 . . . . . . . . . . . 12 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑣 ∈ (1st𝐵)) → 𝑣Q)
3228, 30, 31syl2anc 397 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣Q)
33 simplrl 495 . . . . . . . . . . . 12 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑤Q)
3433adantr 265 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑤Q)
35 addclnq 6531 . . . . . . . . . . 11 ((𝑣Q𝑤Q) → (𝑣 +Q 𝑤) ∈ Q)
3632, 34, 35syl2anc 397 . . . . . . . . . 10 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑣 +Q 𝑤) ∈ Q)
37 addclnq 6531 . . . . . . . . . 10 ((𝑢Q ∧ (𝑣 +Q 𝑤) ∈ Q) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q)
3827, 36, 37syl2anc 397 . . . . . . . . 9 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q)
39 prdisj 6648 . . . . . . . . 9 ((⟨(1st ‘(𝐴 +P 𝐵)), (2nd ‘(𝐴 +P 𝐵))⟩ ∈ P ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q) → ¬ ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵))))
4023, 38, 39syl2anc 397 . . . . . . . 8 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ¬ ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵))))
4118adantr 265 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐴P)
4219adantr 265 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐵P)
43 simplrl 495 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑢 ∈ (1st𝐴))
44 simplrr 496 . . . . . . . . . . 11 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝑣 +Q 𝑤) ∈ (1st𝐵))
4544ad2antrr 465 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑣 +Q 𝑤) ∈ (1st𝐵))
46 df-iplp 6624 . . . . . . . . . . . 12 +P = (𝑟P, 𝑠P ↦ ⟨{𝑓Q ∣ ∃𝑔QQ (𝑔 ∈ (1st𝑟) ∧ ∈ (1st𝑠) ∧ 𝑓 = (𝑔 +Q ))}, {𝑓Q ∣ ∃𝑔QQ (𝑔 ∈ (2nd𝑟) ∧ ∈ (2nd𝑠) ∧ 𝑓 = (𝑔 +Q ))}⟩)
47 addclnq 6531 . . . . . . . . . . . 12 ((𝑔QQ) → (𝑔 +Q ) ∈ Q)
4846, 47genpprecll 6670 . . . . . . . . . . 11 ((𝐴P𝐵P) → ((𝑢 ∈ (1st𝐴) ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵))))
4948imp 119 . . . . . . . . . 10 (((𝐴P𝐵P) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)))
5041, 42, 43, 45, 49syl22anc 1147 . . . . . . . . 9 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)))
5127adantr 265 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑢Q)
5214ad2antrr 465 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑡Q)
5332adantr 265 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑣Q)
54 addcomnqg 6537 . . . . . . . . . . . . . 14 ((𝑓Q𝑔Q) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
5554adantl 266 . . . . . . . . . . . . 13 (((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) ∧ (𝑓Q𝑔Q)) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
56 addassnqg 6538 . . . . . . . . . . . . . 14 ((𝑓Q𝑔QQ) → ((𝑓 +Q 𝑔) +Q ) = (𝑓 +Q (𝑔 +Q )))
5756adantl 266 . . . . . . . . . . . . 13 (((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) ∧ (𝑓Q𝑔QQ)) → ((𝑓 +Q 𝑔) +Q ) = (𝑓 +Q (𝑔 +Q )))
58 addclnq 6531 . . . . . . . . . . . . . 14 ((𝑓Q𝑔Q) → (𝑓 +Q 𝑔) ∈ Q)
5958adantl 266 . . . . . . . . . . . . 13 (((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) ∧ (𝑓Q𝑔Q)) → (𝑓 +Q 𝑔) ∈ Q)
6051, 52, 53, 55, 57, 52, 59caov4d 5713 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) = ((𝑢 +Q 𝑣) +Q (𝑡 +Q 𝑡)))
61 simprr 492 . . . . . . . . . . . . . 14 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝑡 +Q 𝑡) = 𝑤)
6261ad2antrr 465 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑡 +Q 𝑡) = 𝑤)
6362oveq2d 5556 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑣) +Q (𝑡 +Q 𝑡)) = ((𝑢 +Q 𝑣) +Q 𝑤))
6433ad2antrr 465 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑤Q)
65 addassnqg 6538 . . . . . . . . . . . . 13 ((𝑢Q𝑣Q𝑤Q) → ((𝑢 +Q 𝑣) +Q 𝑤) = (𝑢 +Q (𝑣 +Q 𝑤)))
6651, 53, 64, 65syl3anc 1146 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑣) +Q 𝑤) = (𝑢 +Q (𝑣 +Q 𝑤)))
6760, 63, 663eqtrd 2092 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) = (𝑢 +Q (𝑣 +Q 𝑤)))
68 simplrr 496 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q 𝑡) ∈ (2nd𝐴))
69 simpr 107 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑣 +Q 𝑡) ∈ (2nd𝐶))
7017simp3d 929 . . . . . . . . . . . . . 14 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐶P)
7170adantr 265 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐶P)
7246, 47genppreclu 6671 . . . . . . . . . . . . 13 ((𝐴P𝐶P) → (((𝑢 +Q 𝑡) ∈ (2nd𝐴) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) ∈ (2nd ‘(𝐴 +P 𝐶))))
7341, 71, 72syl2anc 397 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (((𝑢 +Q 𝑡) ∈ (2nd𝐴) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) ∈ (2nd ‘(𝐴 +P 𝐶))))
7468, 69, 73mp2and 417 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) ∈ (2nd ‘(𝐴 +P 𝐶)))
7567, 74eqeltrrd 2131 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐶)))
76 simpr 107 . . . . . . . . . . . . 13 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
7776ad3antrrr 469 . . . . . . . . . . . 12 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
7877ad2antrr 465 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
79 fveq2 5206 . . . . . . . . . . . 12 ((𝐴 +P 𝐵) = (𝐴 +P 𝐶) → (2nd ‘(𝐴 +P 𝐵)) = (2nd ‘(𝐴 +P 𝐶)))
8079eleq2d 2123 . . . . . . . . . . 11 ((𝐴 +P 𝐵) = (𝐴 +P 𝐶) → ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵)) ↔ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐶))))
8178, 80syl 14 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵)) ↔ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐶))))
8275, 81mpbird 160 . . . . . . . . 9 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵)))
8350, 82jca 294 . . . . . . . 8 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵))))
8440, 83mtand 601 . . . . . . 7 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ¬ (𝑣 +Q 𝑡) ∈ (2nd𝐶))
85 prop 6631 . . . . . . . . 9 (𝐶P → ⟨(1st𝐶), (2nd𝐶)⟩ ∈ P)
8670, 85syl 14 . . . . . . . 8 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ⟨(1st𝐶), (2nd𝐶)⟩ ∈ P)
87 simplrl 495 . . . . . . . . 9 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑡Q)
88 ltaddnq 6563 . . . . . . . . 9 ((𝑣Q𝑡Q) → 𝑣 <Q (𝑣 +Q 𝑡))
8932, 87, 88syl2anc 397 . . . . . . . 8 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 <Q (𝑣 +Q 𝑡))
90 prloc 6647 . . . . . . . 8 ((⟨(1st𝐶), (2nd𝐶)⟩ ∈ P𝑣 <Q (𝑣 +Q 𝑡)) → (𝑣 ∈ (1st𝐶) ∨ (𝑣 +Q 𝑡) ∈ (2nd𝐶)))
9186, 89, 90syl2anc 397 . . . . . . 7 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑣 ∈ (1st𝐶) ∨ (𝑣 +Q 𝑡) ∈ (2nd𝐶)))
9284, 91ecased 1255 . . . . . 6 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 ∈ (1st𝐶))
9316, 92rexlimddv 2454 . . . . 5 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑣 ∈ (1st𝐶))
948, 93rexlimddv 2454 . . . 4 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑣 ∈ (1st𝐶))
955, 94rexlimddv 2454 . . 3 ((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) → 𝑣 ∈ (1st𝐶))
9695ex 112 . 2 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (𝑣 ∈ (1st𝐵) → 𝑣 ∈ (1st𝐶)))
9796ssrdv 2979 1 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (1st𝐵) ⊆ (1st𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 101  wb 102  wo 639  w3a 896   = wceq 1259  wcel 1409  wrex 2324  wss 2945  cop 3406   class class class wbr 3792  cfv 4930  (class class class)co 5540  1st c1st 5793  2nd c2nd 5794  Qcnq 6436   +Q cplq 6438   <Q cltq 6441  Pcnp 6447   +P cpp 6449
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-in1 554  ax-in2 555  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-coll 3900  ax-sep 3903  ax-nul 3911  ax-pow 3955  ax-pr 3972  ax-un 4198  ax-setind 4290  ax-iinf 4339
This theorem depends on definitions:  df-bi 114  df-dc 754  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  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-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2788  df-csb 2881  df-dif 2948  df-un 2950  df-in 2952  df-ss 2959  df-nul 3253  df-pw 3389  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-int 3644  df-iun 3687  df-br 3793  df-opab 3847  df-mpt 3848  df-tr 3883  df-eprel 4054  df-id 4058  df-po 4061  df-iso 4062  df-iord 4131  df-on 4133  df-suc 4136  df-iom 4342  df-xp 4379  df-rel 4380  df-cnv 4381  df-co 4382  df-dm 4383  df-rn 4384  df-res 4385  df-ima 4386  df-iota 4895  df-fun 4932  df-fn 4933  df-f 4934  df-f1 4935  df-fo 4936  df-f1o 4937  df-fv 4938  df-ov 5543  df-oprab 5544  df-mpt2 5545  df-1st 5795  df-2nd 5796  df-recs 5951  df-irdg 5988  df-1o 6032  df-2o 6033  df-oadd 6036  df-omul 6037  df-er 6137  df-ec 6139  df-qs 6143  df-ni 6460  df-pli 6461  df-mi 6462  df-lti 6463  df-plpq 6500  df-mpq 6501  df-enq 6503  df-nqqs 6504  df-plqqs 6505  df-mqqs 6506  df-1nqqs 6507  df-rq 6508  df-ltnqqs 6509  df-enq0 6580  df-nq0 6581  df-0nq0 6582  df-plq0 6583  df-mq0 6584  df-inp 6622  df-iplp 6624
This theorem is referenced by:  addcanprg  6772
  Copyright terms: Public domain W3C validator