MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frgra3vlem1 Structured version   Visualization version   GIF version

Theorem frgra3vlem1 26293
Description: Lemma 1 for frgra3v 26295. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
Assertion
Ref Expression
frgra3vlem1 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ∀𝑥𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → 𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐸,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝑥,𝑍,𝑦

Proof of Theorem frgra3vlem1
StepHypRef Expression
1 vex 3175 . . . . . 6 𝑥 ∈ V
21eltp 4176 . . . . 5 (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶))
3 vex 3175 . . . . . . . . 9 𝑦 ∈ V
43eltp 4176 . . . . . . . 8 (𝑦 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶))
5 eqidd 2610 . . . . . . . . . . . . . . 15 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐴)
65a1i 11 . . . . . . . . . . . . . 14 ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐴))
762a1i 12 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐴))))
8 preq1 4211 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → {𝑦, 𝐴} = {𝐴, 𝐴})
9 preq1 4211 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → {𝑦, 𝐵} = {𝐴, 𝐵})
108, 9preq12d 4219 . . . . . . . . . . . . . 14 (𝑦 = 𝐴 → {{𝑦, 𝐴}, {𝑦, 𝐵}} = {{𝐴, 𝐴}, {𝐴, 𝐵}})
1110sseq1d 3594 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸))
12 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → (𝐴 = 𝑦𝐴 = 𝐴))
1312imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐴 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐴)))
1413imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦)) ↔ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐴))))
157, 11, 143imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐴 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦))))
16 prex 4831 . . . . . . . . . . . . . . . . 17 {𝐴, 𝐴} ∈ V
17 prex 4831 . . . . . . . . . . . . . . . . 17 {𝐴, 𝐵} ∈ V
1816, 17prss 4290 . . . . . . . . . . . . . . . 16 (({𝐴, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ↔ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸)
19 usgraedgrn 25676 . . . . . . . . . . . . . . . . . . 19 (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐴𝐴)
20 df-ne 2781 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝐴 ↔ ¬ 𝐴 = 𝐴)
21 eqid 2609 . . . . . . . . . . . . . . . . . . . . 21 𝐴 = 𝐴
2221pm2.24i 144 . . . . . . . . . . . . . . . . . . . 20 𝐴 = 𝐴𝐴 = 𝐵)
2320, 22sylbi 205 . . . . . . . . . . . . . . . . . . 19 (𝐴𝐴𝐴 = 𝐵)
2419, 23syl 17 . . . . . . . . . . . . . . . . . 18 (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝐵)
2524expcom 449 . . . . . . . . . . . . . . . . 17 ({𝐴, 𝐴} ∈ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐴 = 𝐵))
2625adantr 479 . . . . . . . . . . . . . . . 16 (({𝐴, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐴 = 𝐵))
2718, 26sylbir 223 . . . . . . . . . . . . . . 15 ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐴 = 𝐵))
2827adantld 481 . . . . . . . . . . . . . 14 ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐵))
29282a1i 12 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐵))))
30 preq1 4211 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → {𝑦, 𝐴} = {𝐵, 𝐴})
31 preq1 4211 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → {𝑦, 𝐵} = {𝐵, 𝐵})
3230, 31preq12d 4219 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → {{𝑦, 𝐴}, {𝑦, 𝐵}} = {{𝐵, 𝐴}, {𝐵, 𝐵}})
3332sseq1d 3594 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸))
34 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → (𝐴 = 𝑦𝐴 = 𝐵))
3534imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐵)))
3635imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦)) ↔ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐵))))
3729, 33, 363imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦))))
3821pm2.24i 144 . . . . . . . . . . . . . . . . . . . 20 𝐴 = 𝐴𝐴 = 𝐶)
3920, 38sylbi 205 . . . . . . . . . . . . . . . . . . 19 (𝐴𝐴𝐴 = 𝐶)
4019, 39syl 17 . . . . . . . . . . . . . . . . . 18 (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝐶)
4140expcom 449 . . . . . . . . . . . . . . . . 17 ({𝐴, 𝐴} ∈ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐴 = 𝐶))
4241adantr 479 . . . . . . . . . . . . . . . 16 (({𝐴, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐴 = 𝐶))
4318, 42sylbir 223 . . . . . . . . . . . . . . 15 ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐴 = 𝐶))
4443adantld 481 . . . . . . . . . . . . . 14 ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐶))
45442a1i 12 . . . . . . . . . . . . 13 (𝑦 = 𝐶 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐶))))
46 preq1 4211 . . . . . . . . . . . . . . 15 (𝑦 = 𝐶 → {𝑦, 𝐴} = {𝐶, 𝐴})
47 preq1 4211 . . . . . . . . . . . . . . 15 (𝑦 = 𝐶 → {𝑦, 𝐵} = {𝐶, 𝐵})
4846, 47preq12d 4219 . . . . . . . . . . . . . 14 (𝑦 = 𝐶 → {{𝑦, 𝐴}, {𝑦, 𝐵}} = {{𝐶, 𝐴}, {𝐶, 𝐵}})
4948sseq1d 3594 . . . . . . . . . . . . 13 (𝑦 = 𝐶 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸))
50 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐶 → (𝐴 = 𝑦𝐴 = 𝐶))
5150imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐶 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐶)))
5251imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐶 → (({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦)) ↔ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝐶))))
5345, 49, 523imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐶 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦))))
5415, 37, 533jaoi 1382 . . . . . . . . . . 11 ((𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶) → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦))))
55 preq1 4211 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → {𝑥, 𝐴} = {𝐴, 𝐴})
56 preq1 4211 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
5755, 56preq12d 4219 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝐴, 𝐴}, {𝐴, 𝐵}})
5857sseq1d 3594 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸))
59 eqeq1 2613 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝑥 = 𝑦𝐴 = 𝑦))
6059imbi2d 328 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦)))
6158, 60imbi12d 332 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)) ↔ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦))))
6261imbi2d 328 . . . . . . . . . . 11 (𝑥 = 𝐴 → (({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦))) ↔ ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 = 𝑦)))))
6354, 62syl5ibr 234 . . . . . . . . . 10 (𝑥 = 𝐴 → ((𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶) → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)))))
64 prex 4831 . . . . . . . . . . . . . . . . 17 {𝐵, 𝐴} ∈ V
65 prex 4831 . . . . . . . . . . . . . . . . 17 {𝐵, 𝐵} ∈ V
6664, 65prss 4290 . . . . . . . . . . . . . . . 16 (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) ↔ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸)
67 usgraedgrn 25676 . . . . . . . . . . . . . . . . . . 19 (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → 𝐵𝐵)
68 df-ne 2781 . . . . . . . . . . . . . . . . . . . 20 (𝐵𝐵 ↔ ¬ 𝐵 = 𝐵)
69 eqid 2609 . . . . . . . . . . . . . . . . . . . . 21 𝐵 = 𝐵
7069pm2.24i 144 . . . . . . . . . . . . . . . . . . . 20 𝐵 = 𝐵𝐵 = 𝐴)
7168, 70sylbi 205 . . . . . . . . . . . . . . . . . . 19 (𝐵𝐵𝐵 = 𝐴)
7267, 71syl 17 . . . . . . . . . . . . . . . . . 18 (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐴)
7372expcom 449 . . . . . . . . . . . . . . . . 17 ({𝐵, 𝐵} ∈ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐵 = 𝐴))
7473adantl 480 . . . . . . . . . . . . . . . 16 (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐵 = 𝐴))
7566, 74sylbir 223 . . . . . . . . . . . . . . 15 ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐵 = 𝐴))
7675adantld 481 . . . . . . . . . . . . . 14 ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐴))
77762a1i 12 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐴))))
78 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → (𝐵 = 𝑦𝐵 = 𝐴))
7978imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐴 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐴)))
8079imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦)) ↔ ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐴))))
8177, 11, 803imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐴 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦))))
82 eqidd 2610 . . . . . . . . . . . . . . 15 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐵)
8382a1i 11 . . . . . . . . . . . . . 14 ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐵))
84832a1i 12 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐵))))
85 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → (𝐵 = 𝑦𝐵 = 𝐵))
8685imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐵)))
8786imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦)) ↔ ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐵))))
8884, 33, 873imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦))))
8969pm2.24i 144 . . . . . . . . . . . . . . . . . . . 20 𝐵 = 𝐵𝐵 = 𝐶)
9068, 89sylbi 205 . . . . . . . . . . . . . . . . . . 19 (𝐵𝐵𝐵 = 𝐶)
9167, 90syl 17 . . . . . . . . . . . . . . . . . 18 (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐶)
9291expcom 449 . . . . . . . . . . . . . . . . 17 ({𝐵, 𝐵} ∈ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐵 = 𝐶))
9392adantl 480 . . . . . . . . . . . . . . . 16 (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐵 = 𝐶))
9466, 93sylbir 223 . . . . . . . . . . . . . . 15 ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐵 = 𝐶))
9594adantld 481 . . . . . . . . . . . . . 14 ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐶))
96952a1i 12 . . . . . . . . . . . . 13 (𝑦 = 𝐶 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐶))))
97 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
9897imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐶 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐶)))
9998imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐶 → (({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦)) ↔ ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝐶))))
10096, 49, 993imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐶 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦))))
10181, 88, 1003jaoi 1382 . . . . . . . . . . 11 ((𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶) → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦))))
102 preq1 4211 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → {𝑥, 𝐴} = {𝐵, 𝐴})
103 preq1 4211 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → {𝑥, 𝐵} = {𝐵, 𝐵})
104102, 103preq12d 4219 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝐵, 𝐴}, {𝐵, 𝐵}})
105104sseq1d 3594 . . . . . . . . . . . . 13 (𝑥 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸))
106 eqeq1 2613 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
107106imbi2d 328 . . . . . . . . . . . . 13 (𝑥 = 𝐵 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦)))
108105, 107imbi12d 332 . . . . . . . . . . . 12 (𝑥 = 𝐵 → (({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)) ↔ ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦))))
109108imbi2d 328 . . . . . . . . . . 11 (𝑥 = 𝐵 → (({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦))) ↔ ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 = 𝑦)))))
110101, 109syl5ibr 234 . . . . . . . . . 10 (𝑥 = 𝐵 → ((𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶) → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)))))
11121pm2.24i 144 . . . . . . . . . . . . . . . . . . . . 21 𝐴 = 𝐴𝐶 = 𝐴)
11220, 111sylbi 205 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝐴𝐶 = 𝐴)
11319, 112syl 17 . . . . . . . . . . . . . . . . . . 19 (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐶 = 𝐴)
114113expcom 449 . . . . . . . . . . . . . . . . . 18 ({𝐴, 𝐴} ∈ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐶 = 𝐴))
115114adantr 479 . . . . . . . . . . . . . . . . 17 (({𝐴, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐶 = 𝐴))
11618, 115sylbir 223 . . . . . . . . . . . . . . . 16 ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸𝐶 = 𝐴))
117116adantld 481 . . . . . . . . . . . . . . 15 ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐴))
118117a1d 25 . . . . . . . . . . . . . 14 ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐴)))
119118a1i 11 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐴))))
120 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → (𝐶 = 𝑦𝐶 = 𝐴))
121120imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐴 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐴)))
122121imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦)) ↔ ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐴))))
123119, 11, 1223imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐴 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦))))
124 pm2.21 118 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐵 = 𝐵 → (𝐵 = 𝐵 → ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐶 = 𝐵)))
12568, 124sylbi 205 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵𝐵 → (𝐵 = 𝐵 → ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐶 = 𝐵)))
12667, 69, 125mpisyl 21 . . . . . . . . . . . . . . . . . . . . . 22 (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐶 = 𝐵))
127126expcom 449 . . . . . . . . . . . . . . . . . . . . 21 ({𝐵, 𝐵} ∈ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐶 = 𝐵)))
128127adantl 480 . . . . . . . . . . . . . . . . . . . 20 (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐶 = 𝐵)))
12966, 128sylbir 223 . . . . . . . . . . . . . . . . . . 19 ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐶 = 𝐵)))
130129com13 85 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸𝐶 = 𝐵)))
131130adantr 479 . . . . . . . . . . . . . . . . 17 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸𝐶 = 𝐵)))
132131imp 443 . . . . . . . . . . . . . . . 16 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸𝐶 = 𝐵))
133132com12 32 . . . . . . . . . . . . . . 15 ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐵))
134133a1d 25 . . . . . . . . . . . . . 14 ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐵)))
135134a1i 11 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐵))))
136 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → (𝐶 = 𝑦𝐶 = 𝐵))
137136imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐵)))
138137imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦)) ↔ ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐵))))
139135, 33, 1383imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦))))
140 eqidd 2610 . . . . . . . . . . . . . . 15 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐶)
141140a1i 11 . . . . . . . . . . . . . 14 ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐶))
1421412a1i 12 . . . . . . . . . . . . 13 (𝑦 = 𝐶 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐶))))
143 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑦 = 𝐶 → (𝐶 = 𝑦𝐶 = 𝐶))
144143imbi2d 328 . . . . . . . . . . . . . 14 (𝑦 = 𝐶 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐶)))
145144imbi2d 328 . . . . . . . . . . . . 13 (𝑦 = 𝐶 → (({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦)) ↔ ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝐶))))
146142, 49, 1453imtr4d 281 . . . . . . . . . . . 12 (𝑦 = 𝐶 → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦))))
147123, 139, 1463jaoi 1382 . . . . . . . . . . 11 ((𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶) → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦))))
148 preq1 4211 . . . . . . . . . . . . . . 15 (𝑥 = 𝐶 → {𝑥, 𝐴} = {𝐶, 𝐴})
149 preq1 4211 . . . . . . . . . . . . . . 15 (𝑥 = 𝐶 → {𝑥, 𝐵} = {𝐶, 𝐵})
150148, 149preq12d 4219 . . . . . . . . . . . . . 14 (𝑥 = 𝐶 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝐶, 𝐴}, {𝐶, 𝐵}})
151150sseq1d 3594 . . . . . . . . . . . . 13 (𝑥 = 𝐶 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸))
152 eqeq1 2613 . . . . . . . . . . . . . 14 (𝑥 = 𝐶 → (𝑥 = 𝑦𝐶 = 𝑦))
153152imbi2d 328 . . . . . . . . . . . . 13 (𝑥 = 𝐶 → (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦) ↔ ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦)))
154151, 153imbi12d 332 . . . . . . . . . . . 12 (𝑥 = 𝐶 → (({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)) ↔ ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦))))
155154imbi2d 328 . . . . . . . . . . 11 (𝑥 = 𝐶 → (({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦))) ↔ ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐶 = 𝑦)))))
156147, 155syl5ibr 234 . . . . . . . . . 10 (𝑥 = 𝐶 → ((𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶) → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)))))
15763, 110, 1563jaoi 1382 . . . . . . . . 9 ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → ((𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶) → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)))))
158157com3l 86 . . . . . . . 8 ((𝑦 = 𝐴𝑦 = 𝐵𝑦 = 𝐶) → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)))))
1594, 158sylbi 205 . . . . . . 7 (𝑦 ∈ {𝐴, 𝐵, 𝐶} → ({{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸 → ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦)))))
160159imp 443 . . . . . 6 ((𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸) → ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦))))
161160com3l 86 . . . . 5 ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸) → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦))))
1622, 161sylbi 205 . . . 4 (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸) → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦))))
163162imp31 446 . . 3 (((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝑥 = 𝑦))
164163com12 32 . 2 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → 𝑥 = 𝑦))
165164alrimivv 1842 1 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ∀𝑥𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → 𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3o 1029  w3a 1030  wal 1472   = wceq 1474  wcel 1976  wne 2779  wss 3539  {cpr 4126  {ctp 4128   class class class wbr 4577  ran crn 5029   USGrph cusg 25625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-2 10926  df-n0 11140  df-z 11211  df-uz 11520  df-fz 12153  df-hash 12935  df-usgra 25628
This theorem is referenced by:  frgra3vlem2  26294
  Copyright terms: Public domain W3C validator