Theorem frgra3v 26529

Description: Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.)

Assertion

Ref	Expression
frgra3v	⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))))

Proof of Theorem frgra3v

Dummy variables 𝑘 𝑙 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		usgrav 25867	. . . . . 6 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐵, 𝐶} ∈ V ∧ 𝐸 ∈ V))
2		isfrgra 26517	. . . . . 6 ⊢ (({𝐴, 𝐵, 𝐶} ∈ V ∧ 𝐸 ∈ V) → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
3	1, 2	syl 17	. . . . 5 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
4	3	adantl 481	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
5		ibar 524	. . . . 5 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
6	5	adantl 481	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
7	4, 6	bitr4d 270	. . 3 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸))
8		sneq 4135	. . . . . . . . 9 ⊢ (𝑘 = 𝐴 → {𝑘} = {𝐴})
9	8	difeq2d 3690	. . . . . . . 8 ⊢ (𝑘 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
10		preq2 4213	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐴 → {𝑥, 𝑘} = {𝑥, 𝐴})
11	10	preq1d 4218	. . . . . . . . . 10 ⊢ (𝑘 = 𝐴 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝑙}})
12	11	sseq1d 3595	. . . . . . . . 9 ⊢ (𝑘 = 𝐴 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸))
13	12	reubidv 3103	. . . . . . . 8 ⊢ (𝑘 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸))
14	9, 13	raleqbidv 3129	. . . . . . 7 ⊢ (𝑘 = 𝐴 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸))
15		sneq 4135	. . . . . . . . 9 ⊢ (𝑘 = 𝐵 → {𝑘} = {𝐵})
16	15	difeq2d 3690	. . . . . . . 8 ⊢ (𝑘 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
17		preq2 4213	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐵 → {𝑥, 𝑘} = {𝑥, 𝐵})
18	17	preq1d 4218	. . . . . . . . . 10 ⊢ (𝑘 = 𝐵 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝑙}})
19	18	sseq1d 3595	. . . . . . . . 9 ⊢ (𝑘 = 𝐵 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸))
20	19	reubidv 3103	. . . . . . . 8 ⊢ (𝑘 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸))
21	16, 20	raleqbidv 3129	. . . . . . 7 ⊢ (𝑘 = 𝐵 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸))
22		sneq 4135	. . . . . . . . 9 ⊢ (𝑘 = 𝐶 → {𝑘} = {𝐶})
23	22	difeq2d 3690	. . . . . . . 8 ⊢ (𝑘 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
24		preq2 4213	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐶 → {𝑥, 𝑘} = {𝑥, 𝐶})
25	24	preq1d 4218	. . . . . . . . . 10 ⊢ (𝑘 = 𝐶 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝑙}})
26	25	sseq1d 3595	. . . . . . . . 9 ⊢ (𝑘 = 𝐶 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸))
27	26	reubidv 3103	. . . . . . . 8 ⊢ (𝑘 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸))
28	23, 27	raleqbidv 3129	. . . . . . 7 ⊢ (𝑘 = 𝐶 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸))
29	14, 21, 28	raltpg 4183	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
30	29	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
31	30	adantr 480	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
32		tprot 4228	. . . . . . . . . . 11 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
33	32	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
34	33	difeq1d 3689	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
35		necom 2835	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
36	35	biimpi 205	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴)
37		necom 2835	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴)
38	37	biimpi 205	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 𝐶 → 𝐶 ≠ 𝐴)
39	36, 38	anim12i 588	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
40	39	3adant3 1074	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
41		diftpsn3 4273	. . . . . . . . . 10 ⊢ ((𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
42	40, 41	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
43	34, 42	eqtrd 2644	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
44	43	raleqdv 3121	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸))
45		tprot 4228	. . . . . . . . . . . 12 ⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
46	45	eqcomi 2619	. . . . . . . . . . 11 ⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
47	46	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
48	47	difeq1d 3689	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
49		id 22	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵)
50		necom 2835	. . . . . . . . . . . . 13 ⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵)
51	50	biimpi 205	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ 𝐶 → 𝐶 ≠ 𝐵)
52	49, 51	anim12ci 589	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
53	52	3adant2 1073	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
54		diftpsn3 4273	. . . . . . . . . 10 ⊢ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
55	53, 54	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
56	48, 55	eqtrd 2644	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
57	56	raleqdv 3121	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸))
58		diftpsn3 4273	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
59	58	3adant1 1072	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
60	59	raleqdv 3121	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸))
61	44, 57, 60	3anbi123d 1391	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
62	61	adantl 481	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
63	62	adantr 480	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸)))
64		preq2 4213	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝐵 → {𝑥, 𝑙} = {𝑥, 𝐵})
65	64	preq2d 4219	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐵}})
66	65	sseq1d 3595	. . . . . . . . . 10 ⊢ (𝑙 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸))
67	66	reubidv 3103	. . . . . . . . 9 ⊢ (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸))
68		preq2 4213	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝐶 → {𝑥, 𝑙} = {𝑥, 𝐶})
69	68	preq2d 4219	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐶 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐶}})
70	69	sseq1d 3595	. . . . . . . . . 10 ⊢ (𝑙 = 𝐶 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸))
71	70	reubidv 3103	. . . . . . . . 9 ⊢ (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸))
72	67, 71	ralprg 4181	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸)))
73	72	3adant1 1072	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸)))
74	68	preq2d 4219	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝐶 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐶}})
75	74	sseq1d 3595	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐶 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸))
76	75	reubidv 3103	. . . . . . . . . 10 ⊢ (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸))
77		preq2 4213	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐴 → {𝑥, 𝑙} = {𝑥, 𝐴})
78	77	preq2d 4219	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝐴 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐴}})
79	78	sseq1d 3595	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐴 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸))
80	79	reubidv 3103	. . . . . . . . . 10 ⊢ (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸))
81	76, 80	ralprg 4181	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)))
82	81	ancoms 468	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)))
83	82	3adant2 1073	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)))
84	77	preq2d 4219	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐴 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐴}})
85	84	sseq1d 3595	. . . . . . . . . 10 ⊢ (𝑙 = 𝐴 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸))
86	85	reubidv 3103	. . . . . . . . 9 ⊢ (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸))
87	64	preq2d 4219	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐵 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐵}})
88	87	sseq1d 3595	. . . . . . . . . 10 ⊢ (𝑙 = 𝐵 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸))
89	88	reubidv 3103	. . . . . . . . 9 ⊢ (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸))
90	86, 89	ralprg 4181	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸)))
91	90	3adant3 1074	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸)))
92	73, 83, 91	3anbi123d 1391	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸))))
93	92	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸))))
94	93	adantr 480	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ ran 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸))))
95	31, 63, 94	3bitrd 293	. . 3 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸))))
96		frgra3vlem2 26528	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))))
97	96	imp 444	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))
98		3ancomb 1040	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌))
99		3ancoma 1038	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶))
100		biid 250	. . . . . . . . . 10 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶)
101		biid 250	. . . . . . . . . 10 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐵)
102	100, 101, 50	3anbi123i 1244	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ↔ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵))
103	99, 102	bitri 263	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵))
104	98, 103	anbi12i 729	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)))
105		tpcomb 4230	. . . . . . . 8 ⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
106	105	breq1i 4590	. . . . . . 7 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ↔ {𝐴, 𝐶, 𝐵} USGrph 𝐸)
107		reueq1 3117	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸))
108	105, 107	mp1i 13	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) ∧ {𝐴, 𝐶, 𝐵} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸))
109		frgra3vlem2 26528	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) → ({𝐴, 𝐶, 𝐵} USGrph 𝐸 → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))
110	109	imp 444	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) ∧ {𝐴, 𝐶, 𝐵} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
111	108, 110	bitrd 267	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) ∧ {𝐴, 𝐶, 𝐵} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
112	104, 106, 111	syl2anb 495	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
113	97, 112	anbi12d 743	. . . . 5 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸) ↔ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))
114		3anrot 1036	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋))
115		3anrot 1036	. . . . . . . . 9 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))
116		biid 250	. . . . . . . . . 10 ⊢ (𝐵 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
117	116, 35, 37	3anbi123i 1244	. . . . . . . . 9 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
118	115, 117	bitr3i 265	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
119	114, 118	anbi12i 729	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ↔ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)))
120	32	breq1i 4590	. . . . . . 7 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ↔ {𝐵, 𝐶, 𝐴} USGrph 𝐸)
121		reueq1 3117	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸))
122	32, 121	mp1i 13	. . . . . . . 8 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) ∧ {𝐵, 𝐶, 𝐴} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸))
123		frgra3vlem2 26528	. . . . . . . . 9 ⊢ (((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) → ({𝐵, 𝐶, 𝐴} USGrph 𝐸 → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))))
124	123	imp 444	. . . . . . . 8 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) ∧ {𝐵, 𝐶, 𝐴} USGrph 𝐸) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)))
125	122, 124	bitrd 267	. . . . . . 7 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) ∧ {𝐵, 𝐶, 𝐴} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)))
126	119, 120, 125	syl2anb 495	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)))
127		3ancoma 1038	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍))
128		3ancomb 1040	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶))
129	35, 116, 100	3anbi123i 1244	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶))
130	128, 129	bitri 263	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶))
131	127, 130	anbi12i 729	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ↔ ((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)))
132		tpcoma 4229	. . . . . . . 8 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
133	132	breq1i 4590	. . . . . . 7 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ↔ {𝐵, 𝐴, 𝐶} USGrph 𝐸)
134		reueq1 3117	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸))
135	132, 134	mp1i 13	. . . . . . . 8 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) ∧ {𝐵, 𝐴, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸))
136		frgra3vlem2 26528	. . . . . . . . 9 ⊢ (((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) → ({𝐵, 𝐴, 𝐶} USGrph 𝐸 → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))))
137	136	imp 444	. . . . . . . 8 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) ∧ {𝐵, 𝐴, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
138	135, 137	bitrd 267	. . . . . . 7 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) ∧ {𝐵, 𝐴, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
139	131, 133, 138	syl2anb 495	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
140	126, 139	anbi12d 743	. . . . 5 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))))
141		3anrot 1036	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))
142	141	biimpri 217	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌))
143		3anrot 1036	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵))
144	37, 50, 101	3anbi123i 1244	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ↔ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
145	143, 144	bitri 263	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
146	145	biimpi 205	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
147	142, 146	anim12i 588	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)))
148	46	breq1i 4590	. . . . . . . 8 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ↔ {𝐶, 𝐴, 𝐵} USGrph 𝐸)
149	148	biimpi 205	. . . . . . 7 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → {𝐶, 𝐴, 𝐵} USGrph 𝐸)
150		reueq1 3117	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸))
151	46, 150	mp1i 13	. . . . . . . 8 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝐶, 𝐴, 𝐵} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸))
152		frgra3vlem2 26528	. . . . . . . . 9 ⊢ (((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) → ({𝐶, 𝐴, 𝐵} USGrph 𝐸 → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸))))
153	152	imp 444	. . . . . . . 8 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝐶, 𝐴, 𝐵} USGrph 𝐸) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸)))
154	151, 153	bitrd 267	. . . . . . 7 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝐶, 𝐴, 𝐵} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸)))
155	147, 149, 154	syl2an 493	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ↔ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸)))
156		3anrev 1042	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋))
157	156	biimpi 205	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋))
158	50, 37, 35	3anbi123i 1244	. . . . . . . . . 10 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ↔ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴))
159	158	biimpi 205	. . . . . . . . 9 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) → (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴))
160	159	3com13 1262	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴))
161	157, 160	anim12i 588	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)))
162		tpcoma 4229	. . . . . . . . . 10 ⊢ {𝐵, 𝐶, 𝐴} = {𝐶, 𝐵, 𝐴}
163	32, 162	eqtri 2632	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴}
164	163	breq1i 4590	. . . . . . . 8 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ↔ {𝐶, 𝐵, 𝐴} USGrph 𝐸)
165	164	biimpi 205	. . . . . . 7 ⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → {𝐶, 𝐵, 𝐴} USGrph 𝐸)
166		reueq1 3117	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸))
167	163, 166	mp1i 13	. . . . . . . 8 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)) ∧ {𝐶, 𝐵, 𝐴} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸))
168		frgra3vlem2 26528	. . . . . . . . 9 ⊢ (((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)) → ({𝐶, 𝐵, 𝐴} USGrph 𝐸 → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸))))
169	168	imp 444	. . . . . . . 8 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)) ∧ {𝐶, 𝐵, 𝐴} USGrph 𝐸) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)))
170	167, 169	bitrd 267	. . . . . . 7 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)) ∧ {𝐶, 𝐵, 𝐴} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)))
171	161, 165, 170	syl2an 493	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)))
172	155, 171	anbi12d 743	. . . . 5 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸) ↔ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸))))
173	113, 140, 172	3anbi123d 1391	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸)) ↔ ((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ∧ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)))))
174		prcom 4211	. . . . . . . . . . 11 ⊢ {𝐵, 𝐶} = {𝐶, 𝐵}
175	174	eleq1i 2679	. . . . . . . . . 10 ⊢ ({𝐵, 𝐶} ∈ ran 𝐸 ↔ {𝐶, 𝐵} ∈ ran 𝐸)
176	175	anbi2i 726	. . . . . . . . 9 ⊢ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))
177	176	anbi2i 726	. . . . . . . 8 ⊢ ((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))
178		anandir 868	. . . . . . . 8 ⊢ ((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))
179	177, 178	bitr4i 266	. . . . . . 7 ⊢ ((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ {𝐶, 𝐵} ∈ ran 𝐸))
180		prcom 4211	. . . . . . . . . . 11 ⊢ {𝐶, 𝐴} = {𝐴, 𝐶}
181	180	eleq1i 2679	. . . . . . . . . 10 ⊢ ({𝐶, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐶} ∈ ran 𝐸)
182	181	anbi2i 726	. . . . . . . . 9 ⊢ (({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))
183	182	anbi2i 726	. . . . . . . 8 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)))
184		anandir 868	. . . . . . . 8 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)))
185	183, 184	bitr4i 266	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸))
186		prcom 4211	. . . . . . . . . . 11 ⊢ {𝐴, 𝐵} = {𝐵, 𝐴}
187	186	eleq1i 2679	. . . . . . . . . 10 ⊢ ({𝐴, 𝐵} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸)
188	187	anbi2i 726	. . . . . . . . 9 ⊢ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸))
189	188	anbi2i 726	. . . . . . . 8 ⊢ ((({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) ↔ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸)))
190		anandir 868	. . . . . . . 8 ⊢ ((({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ {𝐵, 𝐴} ∈ ran 𝐸) ↔ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸)))
191	189, 190	bitr4i 266	. . . . . . 7 ⊢ ((({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) ↔ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ {𝐵, 𝐴} ∈ ran 𝐸))
192	179, 185, 191	3anbi123i 1244	. . . . . 6 ⊢ (((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ∧ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸))) ↔ ((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ {𝐵, 𝐴} ∈ ran 𝐸)))
193		df-3an 1033	. . . . . . . 8 ⊢ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ {𝐶, 𝐵} ∈ ran 𝐸))
194		3anrot 1036	. . . . . . . . 9 ⊢ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
195		prcom 4211	. . . . . . . . . . 11 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
196	195	eleq1i 2679	. . . . . . . . . 10 ⊢ ({𝐵, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)
197		prcom 4211	. . . . . . . . . . 11 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
198	197	eleq1i 2679	. . . . . . . . . 10 ⊢ ({𝐶, 𝐵} ∈ ran 𝐸 ↔ {𝐵, 𝐶} ∈ ran 𝐸)
199		biid 250	. . . . . . . . . 10 ⊢ ({𝐶, 𝐴} ∈ ran 𝐸 ↔ {𝐶, 𝐴} ∈ ran 𝐸)
200	196, 198, 199	3anbi123i 1244	. . . . . . . . 9 ⊢ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
201	194, 200	bitri 263	. . . . . . . 8 ⊢ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
202	193, 201	bitr3i 265	. . . . . . 7 ⊢ ((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
203		df-3an 1033	. . . . . . . 8 ⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸))
204		biid 250	. . . . . . . . 9 ⊢ ({𝐴, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)
205		prcom 4211	. . . . . . . . . 10 ⊢ {𝐴, 𝐶} = {𝐶, 𝐴}
206	205	eleq1i 2679	. . . . . . . . 9 ⊢ ({𝐴, 𝐶} ∈ ran 𝐸 ↔ {𝐶, 𝐴} ∈ ran 𝐸)
207	204, 198, 206	3anbi123i 1244	. . . . . . . 8 ⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
208	203, 207	bitr3i 265	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
209		df-3an 1033	. . . . . . . 8 ⊢ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ↔ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ {𝐵, 𝐴} ∈ ran 𝐸))
210		3anrot 1036	. . . . . . . . 9 ⊢ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))
211		3anrot 1036	. . . . . . . . 9 ⊢ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))
212		biid 250	. . . . . . . . . 10 ⊢ ({𝐵, 𝐶} ∈ ran 𝐸 ↔ {𝐵, 𝐶} ∈ ran 𝐸)
213	196, 212, 206	3anbi123i 1244	. . . . . . . . 9 ⊢ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
214	210, 211, 213	3bitri 285	. . . . . . . 8 ⊢ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
215	209, 214	bitr3i 265	. . . . . . 7 ⊢ ((({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ {𝐵, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
216	202, 208, 215	3anbi123i 1244	. . . . . 6 ⊢ (((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ {𝐵, 𝐴} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
217		df-3an 1033	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ↔ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
218		anabs1 846	. . . . . . 7 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
219		anidm 674	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
220	217, 218, 219	3bitri 285	. . . . . 6 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
221	192, 216, 220	3bitri 285	. . . . 5 ⊢ (((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ∧ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸))) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
222	221	a1i 11	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (((({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ∧ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ∧ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸))) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
223	173, 222	bitrd 267	. . 3 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ ran 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ ran 𝐸)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
224	7, 95, 223	3bitrd 293	. 2 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
225	224	ex 449	1 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃!wreu 2898  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  {csn 4125  {cpr 4127  {ctp 4129   class class class wbr 4583  ran crn 5039   USGrph cusg 25859   FriendGrph cfrgra 26515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-hash 12980  df-usgra 25862  df-frgra 26516

This theorem is referenced by:  3vfriswmgra  26532