relcnvfi - Intuitionistic Logic Explorer

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

Theorem relcnvfi 6575

Description: If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.)

**Assertion**
Ref	Expression
relcnvfi	⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ^◡𝐴 ∈ Fin)

**Proof of Theorem relcnvfi**
Step	Hyp	Ref	Expression
1		dfrel2 4835	. . . . 5 ⊢ (Rel 𝐴 ↔ ^◡^◡𝐴 = 𝐴)
2	1	biimpi 118	. . . 4 ⊢ (Rel 𝐴 → ^◡^◡𝐴 = 𝐴)
3	2	adantr 270	. . 3 ⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ^◡^◡𝐴 = 𝐴)
4		simpr 108	. . 3 ⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ Fin)
5	3, 4	eqeltrd 2159	. 2 ⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ^◡^◡𝐴 ∈ Fin)
6		relcnv 4765	. . . 4 ⊢ Rel ^◡𝐴
7		cnvexg 4922	. . . 4 ⊢ (𝐴 ∈ Fin → ^◡𝐴 ∈ V)
8		cnven 6455	. . . 4 ⊢ ((Rel ^◡𝐴 ∧ ^◡𝐴 ∈ V) → ^◡𝐴 ≈ ^◡^◡𝐴)
9	6, 7, 8	sylancr 405	. . 3 ⊢ (𝐴 ∈ Fin → ^◡𝐴 ≈ ^◡^◡𝐴)
10	9	adantl 271	. 2 ⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ^◡𝐴 ≈ ^◡^◡𝐴)
11		enfii 6520	. 2 ⊢ ((^◡^◡𝐴 ∈ Fin ∧ ^◡𝐴 ≈ ^◡^◡𝐴) → ^◡𝐴 ∈ Fin)
12	5, 10, 11	syl2anc 403	1 ⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ^◡𝐴 ∈ Fin)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 102 = wceq 1285 ∈ wcel 1434 Vcvv 2612 class class class wbr 3811 ^◡ccnv 4400 Rel wrel 4406 ≈ cen 6385 Fincfn 6387

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3922 ax-pow 3974 ax-pr 4000 ax-un 4224

This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-v 2614 df-sbc 2827 df-un 2988 df-in 2990 df-ss 2997 df-pw 3408 df-sn 3428 df-pr 3429 df-op 3431 df-uni 3628 df-br 3812 df-opab 3866 df-mpt 3867 df-id 4084 df-xp 4407 df-rel 4408 df-cnv 4409 df-co 4410 df-dm 4411 df-rn 4412 df-res 4413 df-ima 4414 df-iota 4934 df-fun 4971 df-fn 4972 df-f 4973 df-f1 4974 df-fo 4975 df-f1o 4976 df-fv 4977 df-1st 5846 df-2nd 5847 df-er 6222 df-en 6388 df-fin 6390

This theorem is referenced by: funrnfi 6576