Theorem f1o00 6844

Description: One-to-one onto mapping of the empty set. (Contributed by NM, 15-Apr-1998.)

Assertion

Ref	Expression
f1o00	⊢ (𝐹:∅–1-1-onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))

Proof of Theorem f1o00

Step	Hyp	Ref	Expression
1		dff1o4 6817	. 2 ⊢ (𝐹:∅–1-1-onto→𝐴 ↔ (𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴))
2		fn0 6654	. . . . 5 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)
3	2	birani 507	. . . 4 ⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → 𝐹 = ∅)
4		cnveq 5847	. . . . . . . . . 10 ⊢ (𝐹 = ∅ → ◡𝐹 = ◡∅)
5		cnv0 5857	. . . . . . . . . 10 ⊢ ◡∅ = ∅
6	4, 5	eqtrdi 2815	. . . . . . . . 9 ⊢ (𝐹 = ∅ → ◡𝐹 = ∅)
7	2, 6	sylbi 219	. . . . . . . 8 ⊢ (𝐹 Fn ∅ → ◡𝐹 = ∅)
8	7	fneq1d 6616	. . . . . . 7 ⊢ (𝐹 Fn ∅ → (◡𝐹 Fn 𝐴 ↔ ∅ Fn 𝐴))
9	8	biimpa 480	. . . . . 6 ⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → ∅ Fn 𝐴)
10	9	fndmd 6628	. . . . 5 ⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → dom ∅ = 𝐴)
11		dm0 5898	. . . . 5 ⊢ dom ∅ = ∅
12	10, 11	eqtr3di 2814	. . . 4 ⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → 𝐴 = ∅)
13	3, 12	jca 519	. . 3 ⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → (𝐹 = ∅ ∧ 𝐴 = ∅))
14	2	biranri 509	. . . 4 ⊢ ((𝐹 = ∅ ∧ 𝐴 = ∅) → 𝐹 Fn ∅)
15		eqid 2764	. . . . . 6 ⊢ ∅ = ∅
16		fn0 6654	. . . . . 6 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
17	15, 16	mpbir 233	. . . . 5 ⊢ ∅ Fn ∅
18	6	fneq1d 6616	. . . . . 6 ⊢ (𝐹 = ∅ → (◡𝐹 Fn 𝐴 ↔ ∅ Fn 𝐴))
19		fneq2 6615	. . . . . 6 ⊢ (𝐴 = ∅ → (∅ Fn 𝐴 ↔ ∅ Fn ∅))
20	18, 19	sylan9bb 517	. . . . 5 ⊢ ((𝐹 = ∅ ∧ 𝐴 = ∅) → (◡𝐹 Fn 𝐴 ↔ ∅ Fn ∅))
21	17, 20	mpbiri 260	. . . 4 ⊢ ((𝐹 = ∅ ∧ 𝐴 = ∅) → ◡𝐹 Fn 𝐴)
22	14, 21	jca 519	. . 3 ⊢ ((𝐹 = ∅ ∧ 𝐴 = ∅) → (𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴))
23	13, 22	impbii 211	. 2 ⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
24	1, 23	bitri 277	1 ⊢ (𝐹:∅–1-1-onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1562  ∅c0 4287  ^◡ccnv 5648  dom cdm 5649   Fn wfn 6518  –1-1-onto→wf1o 6522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-mo 2568  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530

This theorem is referenced by:  fo00  6845  f1o0  6846  en0  9001  en0ALT  9002  en0r  9003  infn0  9248  symgbas0  19431  derang0  35524  poimirlem28  38152