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

Theorem addcanprleml 6710
Description: Lemma for addcanprg 6712. (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 6571 . . . . . . 7 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
2 prnmaddl 6586 . . . . . . 7 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
31, 2sylan 267 . . . . . 6 ((𝐵P𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
433ad2antl2 1067 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ 𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
54adantlr 446 . . . 4 ((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
6 simprl 483 . . . . . 6 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑤Q)
7 halfnqq 6506 . . . . . 6 (𝑤Q → ∃𝑡Q (𝑡 +Q 𝑡) = 𝑤)
86, 7syl 14 . . . . 5 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → ∃𝑡Q (𝑡 +Q 𝑡) = 𝑤)
9 simplll 485 . . . . . . . . . 10 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → (𝐴P𝐵P𝐶P))
109adantr 261 . . . . . . . . 9 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝐴P𝐵P𝐶P))
1110simp1d 916 . . . . . . . 8 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝐴P)
12 prop 6571 . . . . . . . 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 483 . . . . . . 7 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑡Q)
15 prarloc2 6600 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑡Q) → ∃𝑢 ∈ (1st𝐴)(𝑢 +Q 𝑡) ∈ (2nd𝐴))
1613, 14, 15syl2anc 391 . . . . . 6 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → ∃𝑢 ∈ (1st𝐴)(𝑢 +Q 𝑡) ∈ (2nd𝐴))
179ad2antrr 457 . . . . . . . . . . . 12 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝐴P𝐵P𝐶P))
1817simp1d 916 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐴P)
1917simp2d 917 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐵P)
20 addclpr 6633 . . . . . . . . . . 11 ((𝐴P𝐵P) → (𝐴 +P 𝐵) ∈ P)
2118, 19, 20syl2anc 391 . . . . . . . . . 10 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝐴 +P 𝐵) ∈ P)
22 prop 6571 . . . . . . . . . 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 483 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑢 ∈ (1st𝐴))
26 elprnql 6577 . . . . . . . . . . 11 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑢 ∈ (1st𝐴)) → 𝑢Q)
2724, 25, 26syl2anc 391 . . . . . . . . . 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 482 . . . . . . . . . . . . 13 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑣 ∈ (1st𝐵))
3029ad2antrr 457 . . . . . . . . . . . 12 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 ∈ (1st𝐵))
31 elprnql 6577 . . . . . . . . . . . 12 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑣 ∈ (1st𝐵)) → 𝑣Q)
3228, 30, 31syl2anc 391 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣Q)
33 simplrl 487 . . . . . . . . . . . 12 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑤Q)
3433adantr 261 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑤Q)
35 addclnq 6471 . . . . . . . . . . 11 ((𝑣Q𝑤Q) → (𝑣 +Q 𝑤) ∈ Q)
3632, 34, 35syl2anc 391 . . . . . . . . . 10 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑣 +Q 𝑤) ∈ Q)
37 addclnq 6471 . . . . . . . . . 10 ((𝑢Q ∧ (𝑣 +Q 𝑤) ∈ Q) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q)
3827, 36, 37syl2anc 391 . . . . . . . . 9 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q)
39 prdisj 6588 . . . . . . . . 9 ((⟨(1st ‘(𝐴 +P 𝐵)), (2nd ‘(𝐴 +P 𝐵))⟩ ∈ P ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q) → ¬ ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵))))
4023, 38, 39syl2anc 391 . . . . . . . 8 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ¬ ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵))))
4118adantr 261 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐴P)
4219adantr 261 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐵P)
43 simplrl 487 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑢 ∈ (1st𝐴))
44 simplrr 488 . . . . . . . . . . 11 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝑣 +Q 𝑤) ∈ (1st𝐵))
4544ad2antrr 457 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑣 +Q 𝑤) ∈ (1st𝐵))
46 df-iplp 6564 . . . . . . . . . . . 12 +P = (𝑟P, 𝑠P ↦ ⟨{𝑓Q ∣ ∃𝑔QQ (𝑔 ∈ (1st𝑟) ∧ ∈ (1st𝑠) ∧ 𝑓 = (𝑔 +Q ))}, {𝑓Q ∣ ∃𝑔QQ (𝑔 ∈ (2nd𝑟) ∧ ∈ (2nd𝑠) ∧ 𝑓 = (𝑔 +Q ))}⟩)
47 addclnq 6471 . . . . . . . . . . . 12 ((𝑔QQ) → (𝑔 +Q ) ∈ Q)
4846, 47genpprecll 6610 . . . . . . . . . . 11 ((𝐴P𝐵P) → ((𝑢 ∈ (1st𝐴) ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵))))
4948imp 115 . . . . . . . . . 10 (((𝐴P𝐵P) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)))
5041, 42, 43, 45, 49syl22anc 1136 . . . . . . . . 9 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)))
5127adantr 261 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑢Q)
5214ad2antrr 457 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑡Q)
5332adantr 261 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑣Q)
54 addcomnqg 6477 . . . . . . . . . . . . . 14 ((𝑓Q𝑔Q) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
5554adantl 262 . . . . . . . . . . . . 13 (((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) ∧ (𝑓Q𝑔Q)) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
56 addassnqg 6478 . . . . . . . . . . . . . 14 ((𝑓Q𝑔QQ) → ((𝑓 +Q 𝑔) +Q ) = (𝑓 +Q (𝑔 +Q )))
5756adantl 262 . . . . . . . . . . . . 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 6471 . . . . . . . . . . . . . 14 ((𝑓Q𝑔Q) → (𝑓 +Q 𝑔) ∈ Q)
5958adantl 262 . . . . . . . . . . . . 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 5685 . . . . . . . . . . . 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 484 . . . . . . . . . . . . . 14 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝑡 +Q 𝑡) = 𝑤)
6261ad2antrr 457 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑡 +Q 𝑡) = 𝑤)
6362oveq2d 5528 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑣) +Q (𝑡 +Q 𝑡)) = ((𝑢 +Q 𝑣) +Q 𝑤))
6433ad2antrr 457 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑤Q)
65 addassnqg 6478 . . . . . . . . . . . . 13 ((𝑢Q𝑣Q𝑤Q) → ((𝑢 +Q 𝑣) +Q 𝑤) = (𝑢 +Q (𝑣 +Q 𝑤)))
6651, 53, 64, 65syl3anc 1135 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑣) +Q 𝑤) = (𝑢 +Q (𝑣 +Q 𝑤)))
6760, 63, 663eqtrd 2076 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) = (𝑢 +Q (𝑣 +Q 𝑤)))
68 simplrr 488 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q 𝑡) ∈ (2nd𝐴))
69 simpr 103 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑣 +Q 𝑡) ∈ (2nd𝐶))
7017simp3d 918 . . . . . . . . . . . . . 14 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐶P)
7170adantr 261 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐶P)
7246, 47genppreclu 6611 . . . . . . . . . . . . 13 ((𝐴P𝐶P) → (((𝑢 +Q 𝑡) ∈ (2nd𝐴) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) ∈ (2nd ‘(𝐴 +P 𝐶))))
7341, 71, 72syl2anc 391 . . . . . . . . . . . 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 409 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) ∈ (2nd ‘(𝐴 +P 𝐶)))
7567, 74eqeltrrd 2115 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐶)))
76 simpr 103 . . . . . . . . . . . . 13 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
7776ad3antrrr 461 . . . . . . . . . . . 12 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
7877ad2antrr 457 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
79 fveq2 5178 . . . . . . . . . . . 12 ((𝐴 +P 𝐵) = (𝐴 +P 𝐶) → (2nd ‘(𝐴 +P 𝐵)) = (2nd ‘(𝐴 +P 𝐶)))
8079eleq2d 2107 . . . . . . . . . . 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 156 . . . . . . . . 9 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵)))
8350, 82jca 290 . . . . . . . 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 591 . . . . . . 7 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ¬ (𝑣 +Q 𝑡) ∈ (2nd𝐶))
85 prop 6571 . . . . . . . . 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 487 . . . . . . . . 9 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑡Q)
88 ltaddnq 6503 . . . . . . . . 9 ((𝑣Q𝑡Q) → 𝑣 <Q (𝑣 +Q 𝑡))
8932, 87, 88syl2anc 391 . . . . . . . 8 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 <Q (𝑣 +Q 𝑡))
90 prloc 6587 . . . . . . . 8 ((⟨(1st𝐶), (2nd𝐶)⟩ ∈ P𝑣 <Q (𝑣 +Q 𝑡)) → (𝑣 ∈ (1st𝐶) ∨ (𝑣 +Q 𝑡) ∈ (2nd𝐶)))
9186, 89, 90syl2anc 391 . . . . . . 7 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑣 ∈ (1st𝐶) ∨ (𝑣 +Q 𝑡) ∈ (2nd𝐶)))
9284, 91ecased 1239 . . . . . 6 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 ∈ (1st𝐶))
9316, 92rexlimddv 2437 . . . . 5 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑣 ∈ (1st𝐶))
948, 93rexlimddv 2437 . . . 4 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑣 ∈ (1st𝐶))
955, 94rexlimddv 2437 . . 3 ((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) → 𝑣 ∈ (1st𝐶))
9695ex 108 . 2 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (𝑣 ∈ (1st𝐵) → 𝑣 ∈ (1st𝐶)))
9796ssrdv 2951 1 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (1st𝐵) ⊆ (1st𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 97  wb 98  wo 629  w3a 885   = wceq 1243  wcel 1393  wrex 2307  wss 2917  cop 3378   class class class wbr 3764  cfv 4902  (class class class)co 5512  1st c1st 5765  2nd c2nd 5766  Qcnq 6376   +Q cplq 6378   <Q cltq 6381  Pcnp 6387   +P cpp 6389
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-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311
This theorem depends on definitions:  df-bi 110  df-dc 743  df-3or 886  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-eprel 4026  df-id 4030  df-po 4033  df-iso 4034  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-1o 6001  df-2o 6002  df-oadd 6005  df-omul 6006  df-er 6106  df-ec 6108  df-qs 6112  df-ni 6400  df-pli 6401  df-mi 6402  df-lti 6403  df-plpq 6440  df-mpq 6441  df-enq 6443  df-nqqs 6444  df-plqqs 6445  df-mqqs 6446  df-1nqqs 6447  df-rq 6448  df-ltnqqs 6449  df-enq0 6520  df-nq0 6521  df-0nq0 6522  df-plq0 6523  df-mq0 6524  df-inp 6562  df-iplp 6564
This theorem is referenced by:  addcanprg  6712
  Copyright terms: Public domain W3C validator