Metamath Proof Explorer

Theorem isgrtri

Description: A triangle in a graph. (Contributed by AV, 20-Jul-2025)

Ref Expression
Hypotheses grtri.v ⊢ V = Vtx ⁡ G
grtri.e ⊢ E = Edg ⁡ G
Assertion isgrtri Could not format assertion : No typesetting found for |- ( T e. ( GrTriangles ` G ) <-> E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 grtri.v ⊢ V = Vtx ⁡ G
2 grtri.e ⊢ E = Edg ⁡ G
3 1 2 grtriprop Could not format ( T e. ( GrTriangles ` G ) -> E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) : No typesetting found for |- ( T e. ( GrTriangles ` G ) -> E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) with typecode |-
4 df-tp ⊢ x y z = x y ∪ z
5 prelpwi ⊢ x ∈ V ∧ y ∈ V → x y ∈ 𝒫 V
6 snelpwi ⊢ z ∈ V → z ∈ 𝒫 V
7 5 6 anim12i ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y ∈ 𝒫 V ∧ z ∈ 𝒫 V
8 7 anasss ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y ∈ 𝒫 V ∧ z ∈ 𝒫 V
9 pwuncl ⊢ x y ∈ 𝒫 V ∧ z ∈ 𝒫 V → x y ∪ z ∈ 𝒫 V
10 8 9 syl ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y ∪ z ∈ 𝒫 V
11 4 10 eqeltrid ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y z ∈ 𝒫 V
12 11 adantr ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → x y z ∈ 𝒫 V
13 eleq1 ⊢ T = x y z → T ∈ 𝒫 V ↔ x y z ∈ 𝒫 V
14 13 3ad2ant1 ⊢ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → T ∈ 𝒫 V ↔ x y z ∈ 𝒫 V
15 14 adantl ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → T ∈ 𝒫 V ↔ x y z ∈ 𝒫 V
16 12 15 mpbird ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → T ∈ 𝒫 V
17 ovex ⊢ 0 ..^ 3 ∈ V
18 17 mptex ⊢ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ∈ V
19 18 a1i ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ∈ V
20 3anass ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ↔ x ∈ V ∧ y ∈ V ∧ z ∈ V
21 20 biimpri ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x ∈ V ∧ y ∈ V ∧ z ∈ V
22 fveq2 ⊢ T = x y z → T = x y z
23 22 eqcomd ⊢ T = x y z → x y z = T
24 23 3ad2ant1 ⊢ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → x y z = T
25 simp2 ⊢ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → T = 3
26 24 25 eqtrd ⊢ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → x y z = 3
27 eqid ⊢ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z
28 eqid ⊢ x y z = x y z
29 27 28 tpf1o ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ x y z = 3 → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto x y z
30 21 26 29 syl2an ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto x y z
31 f1oeq3 ⊢ T = x y z → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto T ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto x y z
32 31 3ad2ant1 ⊢ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto T ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto x y z
33 32 adantl ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto T ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto x y z
34 30 33 mpbird ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto T
35 27 tpf1ofv0 ⊢ x ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 = x
36 35 adantr ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 = x
37 27 tpf1ofv1 ⊢ y ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 = y
38 37 adantr ⊢ y ∈ V ∧ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 = y
39 38 adantl ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 = y
40 36 39 preq12d ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 = x y
41 40 eqcomd ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1
42 41 eleq1d ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E
43 27 tpf1ofv2 ⊢ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 = z
44 43 adantl ⊢ y ∈ V ∧ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 = z
45 44 adantl ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 = z
46 36 45 preq12d ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 = x z
47 46 eqcomd ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x z = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2
48 47 eleq1d ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x z ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
49 39 45 preq12d ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 = y z
50 49 eqcomd ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → y z = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2
51 50 eleq1d ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → y z ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
52 42 48 51 3anbi123d ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
53 52 biimpd ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
54 53 2a1d ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → T = x y z → T = 3 → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
55 54 3imp2 ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
56 34 55 jca ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto T ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
57 f1oeq1 ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f : 0 ..^ 3 ⟶ 1-1 onto T ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto T
58 fveq1 ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 0 = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0
59 fveq1 ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 1 = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1
60 58 59 preq12d ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 0 f ⁡ 1 = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1
61 60 eleq1d ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 0 f ⁡ 1 ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E
62 fveq1 ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 2 = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2
63 58 62 preq12d ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 0 f ⁡ 2 = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2
64 63 eleq1d ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 0 f ⁡ 2 ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
65 59 62 preq12d ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 1 f ⁡ 2 = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2
66 65 eleq1d ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 1 f ⁡ 2 ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
67 61 64 66 3anbi123d ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
68 57 67 anbi12d ⊢ f = i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z → f : 0 ..^ 3 ⟶ 1-1 onto T ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E ↔ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z : 0 ..^ 3 ⟶ 1-1 onto T ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 0 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E ∧ i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 1 i ∈ 0 ..^ 3 ⟼ if i = 0 x if i = 1 y z ⁡ 2 ∈ E
69 19 56 68 spcedv ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → ∃ f f : 0 ..^ 3 ⟶ 1-1 onto T ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
70 16 69 jca ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V ∧ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → T ∈ 𝒫 V ∧ ∃ f f : 0 ..^ 3 ⟶ 1-1 onto T ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
71 1 1vgrex ⊢ x ∈ V → G ∈ V
72 1 2 grtri Could not format ( G e. _V -> ( GrTriangles ` G ) = { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) : No typesetting found for |- ( G e. _V -> ( GrTriangles ` G ) = { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) with typecode |-
73 72 eleq2d Could not format ( G e. _V -> ( T e. ( GrTriangles ` G ) <-> T e. { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) ) : No typesetting found for |- ( G e. _V -> ( T e. ( GrTriangles ` G ) <-> T e. { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) ) with typecode |-
74 71 73 syl Could not format ( x e. V -> ( T e. ( GrTriangles ` G ) <-> T e. { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) ) : No typesetting found for |- ( x e. V -> ( T e. ( GrTriangles ` G ) <-> T e. { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) ) with typecode |-
75 f1oeq3 ⊢ t = T → f : 0 ..^ 3 ⟶ 1-1 onto t ↔ f : 0 ..^ 3 ⟶ 1-1 onto T
76 75 anbi1d ⊢ t = T → f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E ↔ f : 0 ..^ 3 ⟶ 1-1 onto T ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
77 76 exbidv ⊢ t = T → ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E ↔ ∃ f f : 0 ..^ 3 ⟶ 1-1 onto T ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
78 77 elrab ⊢ T ∈ t ∈ 𝒫 V | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E ↔ T ∈ 𝒫 V ∧ ∃ f f : 0 ..^ 3 ⟶ 1-1 onto T ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
79 74 78 bitrdi Could not format ( x e. V -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> T /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) ) ) ) : No typesetting found for |- ( x e. V -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> T /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) ) ) ) with typecode |-
80 79 adantr Could not format ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> T /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) ) ) ) : No typesetting found for |- ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> T /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) ) ) ) with typecode |-
81 80 adantr Could not format ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> T /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) ) ) ) : No typesetting found for |- ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> T /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) ) ) ) with typecode |-
82 70 81 mpbird Could not format ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> T e. ( GrTriangles ` G ) ) : No typesetting found for |- ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> T e. ( GrTriangles ` G ) ) with typecode |-
83 82 ex Could not format ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> T e. ( GrTriangles ` G ) ) ) : No typesetting found for |- ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> T e. ( GrTriangles ` G ) ) ) with typecode |-
84 83 rexlimdvva Could not format ( x e. V -> ( E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> T e. ( GrTriangles ` G ) ) ) : No typesetting found for |- ( x e. V -> ( E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> T e. ( GrTriangles ` G ) ) ) with typecode |-
85 84 rexlimiv Could not format ( E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> T e. ( GrTriangles ` G ) ) : No typesetting found for |- ( E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> T e. ( GrTriangles ` G ) ) with typecode |-
86 3 85 impbii Could not format ( T e. ( GrTriangles ` G ) <-> E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) : No typesetting found for |- ( T e. ( GrTriangles ` G ) <-> E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) with typecode |-