brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  kihirnihi-antisym

---

Theorem kihirnihi-antisym 685

Description: {ki'irni'i} is antisymmetric, reducing to {ki'irdu'i}. (Contributed by la korvo, 15-Jul-2025.)

Hypotheses

Ref	Expression
kihirnihi-antisym.0	⊢ ko'a ki'irni'i ko'e
kihirnihi-antisym.1	⊢ ko'e ki'irni'i ko'a

Assertion

Ref	Expression
kihirnihi-antisym	⊢ ko'a ki'irdu'i ko'e

---

Proof of Theorem kihirnihi-antisym Dummy variables da de are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		kihirnihi-antisym.0	. . . . . . . . . . . 12 ⊢ ko'a ki'irni'i ko'e
2		df-kihirnihi 678	. . . . . . . . . . . 12 ⊢ go ko'a ki'irni'i ko'e gi ro da zo'u ro de zo'u da ckini de ko'a na.a ko'e
3	1, 2	bi 101	. . . . . . . . . . 11 ⊢ ro da zo'u ro de zo'u da ckini de ko'a na.a ko'e
4	3	spec1i 229	. . . . . . . . . 10 ⊢ ro de zo'u da ckini de ko'a na.a ko'e
5	4	spec1i 229	. . . . . . . . 9 ⊢ da ckini de ko'a na.a ko'e
6	5	teri 399	. . . . . . . 8 ⊢ ko'a na.a ko'e te ckini de da
7		df-na.a 110	. . . . . . . 8 ⊢ go ko'a na.a ko'e te ckini de da gi ganai ko'a te ckini de da gi ko'e te ckini de da
8	6, 7	bi 101	. . . . . . 7 ⊢ ganai ko'a te ckini de da gi ko'e te ckini de da
9		kihirnihi-antisym.1	. . . . . . . . . . . 12 ⊢ ko'e ki'irni'i ko'a
10		df-kihirnihi 678	. . . . . . . . . . . 12 ⊢ go ko'e ki'irni'i ko'a gi ro da zo'u ro de zo'u da ckini de ko'e na.a ko'a
11	9, 10	bi 101	. . . . . . . . . . 11 ⊢ ro da zo'u ro de zo'u da ckini de ko'e na.a ko'a
12	11	spec1i 229	. . . . . . . . . 10 ⊢ ro de zo'u da ckini de ko'e na.a ko'a
13	12	spec1i 229	. . . . . . . . 9 ⊢ da ckini de ko'e na.a ko'a
14	13	teri 399	. . . . . . . 8 ⊢ ko'e na.a ko'a te ckini de da
15		df-na.a 110	. . . . . . . 8 ⊢ go ko'e na.a ko'a te ckini de da gi ganai ko'e te ckini de da gi ko'a te ckini de da
16	14, 15	bi 101	. . . . . . 7 ⊢ ganai ko'e te ckini de da gi ko'a te ckini de da
17	8, 16	iso 87	. . . . . 6 ⊢ go ko'a te ckini de da gi ko'e te ckini de da
18		df-o 198	. . . . . 6 ⊢ go ko'a .o ko'e te ckini de da gi go ko'a te ckini de da gi ko'e te ckini de da
19	17, 18	bi-rev 102	. . . . 5 ⊢ ko'a .o ko'e te ckini de da
20	19	tei 398	. . . 4 ⊢ da ckini de ko'a .o ko'e
21	20	ax-gen1 224	. . 3 ⊢ ro de zo'u da ckini de ko'a .o ko'e
22	21	ax-gen1 224	. 2 ⊢ ro da zo'u ro de zo'u da ckini de ko'a .o ko'e
23		df-kihirduhi 683	. 2 ⊢ go ko'a ki'irdu'i ko'e gi ro da zo'u ro de zo'u da ckini de ko'a .o ko'e
24	22, 23	bi-rev 102	1 ⊢ ko'a ki'irdu'i ko'e

Colors of variables: sumti selbri bridi

Syntax hints:  tsb 1  tss 2   ganai bgan 9   go bgo 82   na.a sjnaa 109   .o sjo 197   ro brd 222   ckini sbckini 347   te sbt 396   ki'irni'i sbkihirnihi 677   ki'irdu'i sbkihirduhi 682

This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 48  ax-ge-re 49  ax-ge-in 50  ax-gen1 224  ax-spec1 228

This theorem depends on definitions:  df-go 83  df-na.a 110  df-o 198  df-te 397  df-kihirnihi 678  df-kihirduhi 683

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator