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

Theorem addcanprleml 7434
Description: Lemma for addcanprg 7436. (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 7295 . . . . . . 7 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
2 prnmaddl 7310 . . . . . . 7 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
31, 2sylan 281 . . . . . 6 ((𝐵P𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
433ad2antl2 1144 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ 𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
54adantlr 468 . . . 4 ((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) → ∃𝑤Q (𝑣 +Q 𝑤) ∈ (1st𝐵))
6 simprl 520 . . . . . 6 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑤Q)
7 halfnqq 7230 . . . . . 6 (𝑤Q → ∃𝑡Q (𝑡 +Q 𝑡) = 𝑤)
86, 7syl 14 . . . . 5 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → ∃𝑡Q (𝑡 +Q 𝑡) = 𝑤)
9 simplll 522 . . . . . . . . . 10 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → (𝐴P𝐵P𝐶P))
109adantr 274 . . . . . . . . 9 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝐴P𝐵P𝐶P))
1110simp1d 993 . . . . . . . 8 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝐴P)
12 prop 7295 . . . . . . . 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 520 . . . . . . 7 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑡Q)
15 prarloc2 7324 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑡Q) → ∃𝑢 ∈ (1st𝐴)(𝑢 +Q 𝑡) ∈ (2nd𝐴))
1613, 14, 15syl2anc 408 . . . . . 6 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → ∃𝑢 ∈ (1st𝐴)(𝑢 +Q 𝑡) ∈ (2nd𝐴))
179ad2antrr 479 . . . . . . . . . . . 12 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝐴P𝐵P𝐶P))
1817simp1d 993 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐴P)
1917simp2d 994 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐵P)
20 addclpr 7357 . . . . . . . . . . 11 ((𝐴P𝐵P) → (𝐴 +P 𝐵) ∈ P)
2118, 19, 20syl2anc 408 . . . . . . . . . 10 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝐴 +P 𝐵) ∈ P)
22 prop 7295 . . . . . . . . . 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 520 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑢 ∈ (1st𝐴))
26 elprnql 7301 . . . . . . . . . . 11 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑢 ∈ (1st𝐴)) → 𝑢Q)
2724, 25, 26syl2anc 408 . . . . . . . . . 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 519 . . . . . . . . . . . . 13 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑣 ∈ (1st𝐵))
3029ad2antrr 479 . . . . . . . . . . . 12 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 ∈ (1st𝐵))
31 elprnql 7301 . . . . . . . . . . . 12 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑣 ∈ (1st𝐵)) → 𝑣Q)
3228, 30, 31syl2anc 408 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣Q)
33 simplrl 524 . . . . . . . . . . . 12 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑤Q)
3433adantr 274 . . . . . . . . . . 11 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑤Q)
35 addclnq 7195 . . . . . . . . . . 11 ((𝑣Q𝑤Q) → (𝑣 +Q 𝑤) ∈ Q)
3632, 34, 35syl2anc 408 . . . . . . . . . 10 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑣 +Q 𝑤) ∈ Q)
37 addclnq 7195 . . . . . . . . . 10 ((𝑢Q ∧ (𝑣 +Q 𝑤) ∈ Q) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q)
3827, 36, 37syl2anc 408 . . . . . . . . 9 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q)
39 prdisj 7312 . . . . . . . . 9 ((⟨(1st ‘(𝐴 +P 𝐵)), (2nd ‘(𝐴 +P 𝐵))⟩ ∈ P ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ Q) → ¬ ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵))))
4023, 38, 39syl2anc 408 . . . . . . . 8 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ¬ ((𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵))))
4118adantr 274 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐴P)
4219adantr 274 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐵P)
43 simplrl 524 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑢 ∈ (1st𝐴))
44 simplrr 525 . . . . . . . . . . 11 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝑣 +Q 𝑤) ∈ (1st𝐵))
4544ad2antrr 479 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑣 +Q 𝑤) ∈ (1st𝐵))
46 df-iplp 7288 . . . . . . . . . . . 12 +P = (𝑟P, 𝑠P ↦ ⟨{𝑓Q ∣ ∃𝑔QQ (𝑔 ∈ (1st𝑟) ∧ ∈ (1st𝑠) ∧ 𝑓 = (𝑔 +Q ))}, {𝑓Q ∣ ∃𝑔QQ (𝑔 ∈ (2nd𝑟) ∧ ∈ (2nd𝑠) ∧ 𝑓 = (𝑔 +Q ))}⟩)
47 addclnq 7195 . . . . . . . . . . . 12 ((𝑔QQ) → (𝑔 +Q ) ∈ Q)
4846, 47genpprecll 7334 . . . . . . . . . . 11 ((𝐴P𝐵P) → ((𝑢 ∈ (1st𝐴) ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵))))
4948imp 123 . . . . . . . . . 10 (((𝐴P𝐵P) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)))
5041, 42, 43, 45, 49syl22anc 1217 . . . . . . . . 9 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (1st ‘(𝐴 +P 𝐵)))
5127adantr 274 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑢Q)
5214ad2antrr 479 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑡Q)
5332adantr 274 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑣Q)
54 addcomnqg 7201 . . . . . . . . . . . . . 14 ((𝑓Q𝑔Q) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
5554adantl 275 . . . . . . . . . . . . 13 (((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) ∧ (𝑓Q𝑔Q)) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
56 addassnqg 7202 . . . . . . . . . . . . . 14 ((𝑓Q𝑔QQ) → ((𝑓 +Q 𝑔) +Q ) = (𝑓 +Q (𝑔 +Q )))
5756adantl 275 . . . . . . . . . . . . 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 7195 . . . . . . . . . . . . . 14 ((𝑓Q𝑔Q) → (𝑓 +Q 𝑔) ∈ Q)
5958adantl 275 . . . . . . . . . . . . 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 5955 . . . . . . . . . . . 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 521 . . . . . . . . . . . . . 14 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝑡 +Q 𝑡) = 𝑤)
6261ad2antrr 479 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑡 +Q 𝑡) = 𝑤)
6362oveq2d 5790 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑣) +Q (𝑡 +Q 𝑡)) = ((𝑢 +Q 𝑣) +Q 𝑤))
6433ad2antrr 479 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝑤Q)
65 addassnqg 7202 . . . . . . . . . . . . 13 ((𝑢Q𝑣Q𝑤Q) → ((𝑢 +Q 𝑣) +Q 𝑤) = (𝑢 +Q (𝑣 +Q 𝑤)))
6651, 53, 64, 65syl3anc 1216 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑣) +Q 𝑤) = (𝑢 +Q (𝑣 +Q 𝑤)))
6760, 63, 663eqtrd 2176 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) = (𝑢 +Q (𝑣 +Q 𝑤)))
68 simplrr 525 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q 𝑡) ∈ (2nd𝐴))
69 simpr 109 . . . . . . . . . . . 12 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑣 +Q 𝑡) ∈ (2nd𝐶))
7017simp3d 995 . . . . . . . . . . . . . 14 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝐶P)
7170adantr 274 . . . . . . . . . . . . 13 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → 𝐶P)
7246, 47genppreclu 7335 . . . . . . . . . . . . 13 ((𝐴P𝐶P) → (((𝑢 +Q 𝑡) ∈ (2nd𝐴) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) ∈ (2nd ‘(𝐴 +P 𝐶))))
7341, 71, 72syl2anc 408 . . . . . . . . . . . 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 429 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → ((𝑢 +Q 𝑡) +Q (𝑣 +Q 𝑡)) ∈ (2nd ‘(𝐴 +P 𝐶)))
7567, 74eqeltrrd 2217 . . . . . . . . . 10 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐶)))
76 simpr 109 . . . . . . . . . . . . 13 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
7776ad3antrrr 483 . . . . . . . . . . . 12 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
7877ad2antrr 479 . . . . . . . . . . 11 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶))
79 fveq2 5421 . . . . . . . . . . . 12 ((𝐴 +P 𝐵) = (𝐴 +P 𝐶) → (2nd ‘(𝐴 +P 𝐵)) = (2nd ‘(𝐴 +P 𝐶)))
8079eleq2d 2209 . . . . . . . . . . 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 166 . . . . . . . . 9 ((((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) ∧ (𝑣 +Q 𝑡) ∈ (2nd𝐶)) → (𝑢 +Q (𝑣 +Q 𝑤)) ∈ (2nd ‘(𝐴 +P 𝐵)))
8350, 82jca 304 . . . . . . . 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 654 . . . . . . 7 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → ¬ (𝑣 +Q 𝑡) ∈ (2nd𝐶))
85 prop 7295 . . . . . . . . 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 524 . . . . . . . . 9 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑡Q)
88 ltaddnq 7227 . . . . . . . . 9 ((𝑣Q𝑡Q) → 𝑣 <Q (𝑣 +Q 𝑡))
8932, 87, 88syl2anc 408 . . . . . . . 8 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 <Q (𝑣 +Q 𝑡))
90 prloc 7311 . . . . . . . 8 ((⟨(1st𝐶), (2nd𝐶)⟩ ∈ P𝑣 <Q (𝑣 +Q 𝑡)) → (𝑣 ∈ (1st𝐶) ∨ (𝑣 +Q 𝑡) ∈ (2nd𝐶)))
9186, 89, 90syl2anc 408 . . . . . . 7 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → (𝑣 ∈ (1st𝐶) ∨ (𝑣 +Q 𝑡) ∈ (2nd𝐶)))
9284, 91ecased 1327 . . . . . 6 (((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd𝐴))) → 𝑣 ∈ (1st𝐶))
9316, 92rexlimddv 2554 . . . . 5 ((((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) ∧ (𝑡Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → 𝑣 ∈ (1st𝐶))
948, 93rexlimddv 2554 . . . 4 (((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) ∧ (𝑤Q ∧ (𝑣 +Q 𝑤) ∈ (1st𝐵))) → 𝑣 ∈ (1st𝐶))
955, 94rexlimddv 2554 . . 3 ((((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st𝐵)) → 𝑣 ∈ (1st𝐶))
9695ex 114 . 2 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (𝑣 ∈ (1st𝐵) → 𝑣 ∈ (1st𝐶)))
9796ssrdv 3103 1 (((𝐴P𝐵P𝐶P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (1st𝐵) ⊆ (1st𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 697  w3a 962   = wceq 1331  wcel 1480  wrex 2417  wss 3071  cop 3530   class class class wbr 3929  cfv 5123  (class class class)co 5774  1st c1st 6036  2nd c2nd 6037  Qcnq 7100   +Q cplq 7102   <Q cltq 7105  Pcnp 7111   +P cpp 7113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-eprel 4211  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-1o 6313  df-2o 6314  df-oadd 6317  df-omul 6318  df-er 6429  df-ec 6431  df-qs 6435  df-ni 7124  df-pli 7125  df-mi 7126  df-lti 7127  df-plpq 7164  df-mpq 7165  df-enq 7167  df-nqqs 7168  df-plqqs 7169  df-mqqs 7170  df-1nqqs 7171  df-rq 7172  df-ltnqqs 7173  df-enq0 7244  df-nq0 7245  df-0nq0 7246  df-plq0 7247  df-mq0 7248  df-inp 7286  df-iplp 7288
This theorem is referenced by:  addcanprg  7436
  Copyright terms: Public domain W3C validator