Theorem brtpos0 8261

Description: The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). This allows to eliminate sethood hypotheses on 𝐴, 𝐵 in brtpos 8263. (Contributed by Mario Carneiro, 10-Sep-2015.)

Assertion

Ref	Expression
brtpos0	⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴))

Proof of Theorem brtpos0

Step	Hyp	Ref	Expression
1		brtpos2 8260	. 2 ⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ (∅ ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{∅}𝐹𝐴)))
2		ssun2 4179	. . . . 5 ⊢ {∅} ⊆ (◡dom 𝐹 ∪ {∅})
3		0ex 5263	. . . . . 6 ⊢ ∅ ∈ V
4	3	snid 4622	. . . . 5 ⊢ ∅ ∈ {∅}
5	2, 4	sselii 3909	. . . 4 ⊢ ∅ ∈ (◡dom 𝐹 ∪ {∅})
6	5	biantrur 540	. . 3 ⊢ (∪ ◡{∅}𝐹𝐴 ↔ (∅ ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{∅}𝐹𝐴))
7		cnvsn0 6217	. . . . . 6 ⊢ ◡{∅} = ∅
8	7	unieqi 4881	. . . . 5 ⊢ ∪ ◡{∅} = ∪ ∅
9		uni0 4898	. . . . 5 ⊢ ∪ ∅ = ∅
10	8, 9	eqtri 2786	. . . 4 ⊢ ∪ ◡{∅} = ∅
11	10	breq1i 5112	. . 3 ⊢ (∪ ◡{∅}𝐹𝐴 ↔ ∅𝐹𝐴)
12	6, 11	bitr3i 280	. 2 ⊢ ((∅ ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{∅}𝐹𝐴) ↔ ∅𝐹𝐴)
13	1, 12	bitrdi 290	1 ⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146   ∪ cun 4151  ∅c0 4280  {csn 4587  ∪ cuni 4869   class class class wbr 5105  ^◡ccnv 5653  dom cdm 5654  tpos ctpos 8253

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-fv 6554  df-tpos 8254

This theorem is used by:  reldmtpos  8262  brtpos  8263  tpostpos  8274  tposres0  50129