Theorem dftpos4 8225

Description: Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)

Assertion

Ref	Expression
dftpos4	⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))

Distinct variable group:   𝑥,𝐹

Proof of Theorem dftpos4

Dummy variables 𝑦 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-tpos 8206	. . 3 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
2		relcnv 6093	. . . . . . 7 ⊢ Rel ◡dom 𝐹
3		df-rel 5673	. . . . . . 7 ⊢ (Rel ◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V))
4	2, 3	mpbi 229	. . . . . 6 ⊢ ◡dom 𝐹 ⊆ (V × V)
5		unss1 4171	. . . . . 6 ⊢ (◡dom 𝐹 ⊆ (V × V) → (◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}))
6		resmpt 6027	. . . . . 6 ⊢ ((◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}) → ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
7	4, 5, 6	mp2b 10	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})
8		resss 5996	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
9	7, 8	eqsstrri 4009	. . . 4 ⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
10		coss2 5846	. . . 4 ⊢ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) → (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})))
11	9, 10	ax-mp 5	. . 3 ⊢ (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
12	1, 11	eqsstri 4008	. 2 ⊢ tpos 𝐹 ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
13		relco 6097	. . 3 ⊢ Rel (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
14		vex 3470	. . . . 5 ⊢ 𝑦 ∈ V
15		vex 3470	. . . . 5 ⊢ 𝑧 ∈ V
16	14, 15	opelco 5861	. . . 4 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ↔ ∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧))
17		vex 3470	. . . . . . . . 9 ⊢ 𝑤 ∈ V
18		eleq1 2813	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ((V × V) ∪ {∅}) ↔ 𝑦 ∈ ((V × V) ∪ {∅})))
19		sneq 4630	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
20	19	cnveqd 5865	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ◡{𝑥} = ◡{𝑦})
21	20	unieqd 4912	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ∪ ◡{𝑥} = ∪ ◡{𝑦})
22	21	eqeq2d 2735	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑧 = ∪ ◡{𝑥} ↔ 𝑧 = ∪ ◡{𝑦}))
23	18, 22	anbi12d 630	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦})))
24		eqeq1 2728	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (𝑧 = ∪ ◡{𝑦} ↔ 𝑤 = ∪ ◡{𝑦}))
25	24	anbi2d 628	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → ((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦})))
26		df-mpt 5222	. . . . . . . . 9 ⊢ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥})}
27	14, 17, 23, 25, 26	brab 5533	. . . . . . . 8 ⊢ (𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}))
28		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 = ∪ ◡{𝑦})
29	17, 15	breldm 5898	. . . . . . . . . . . . 13 ⊢ (𝑤𝐹𝑧 → 𝑤 ∈ dom 𝐹)
30	29	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 ∈ dom 𝐹)
31	28, 30	eqeltrrd 2826	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦} ∈ dom 𝐹)
32		elvv 5740	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (V × V) ↔ ∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩)
33		opswap 6218	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ◡{⟨𝑧, 𝑤⟩} = ⟨𝑤, 𝑧⟩
34	33	eleq1i 2816	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
35	15, 17	opelcnv 5871	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
36	34, 35	bitr4i 278	. . . . . . . . . . . . . . . 16 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)
37		sneq 4630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → {𝑦} = {⟨𝑧, 𝑤⟩})
38	37	cnveqd 5865	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ◡{𝑦} = ◡{⟨𝑧, 𝑤⟩})
39	38	unieqd 4912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ∪ ◡{𝑦} = ∪ ◡{⟨𝑧, 𝑤⟩})
40	39	eleq1d 2810	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ ∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹))
41		eleq1 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ◡dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹))
42	40, 41	bibi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ((∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹) ↔ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)))
43	36, 42	mpbiri 258	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
44	43	exlimivv 1927	. . . . . . . . . . . . . 14 ⊢ (∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
45	32, 44	sylbi 216	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (V × V) → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
46	45	biimpcd 248	. . . . . . . . . . . 12 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ ◡dom 𝐹))
47		elun1 4168	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ◡dom 𝐹 → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
48	46, 47	syl6 35	. . . . . . . . . . 11 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
49	31, 48	syl 17	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
50		elun2 4169	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
51	50	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
52		simpll 764	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ ((V × V) ∪ {∅}))
53		elun 4140	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((V × V) ∪ {∅}) ↔ (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
54	52, 53	sylib 217	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
55	49, 51, 54	mpjaod 857	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
56		simpr 484	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤𝐹𝑧)
57	28, 56	eqbrtrrd 5162	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦}𝐹𝑧)
58	55, 57	jca 511	. . . . . . . 8 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
59	27, 58	sylanb 580	. . . . . . 7 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
60		brtpos2 8212	. . . . . . . 8 ⊢ (𝑧 ∈ V → (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧)))
61	15, 60	ax-mp 5	. . . . . . 7 ⊢ (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
62	59, 61	sylibr 233	. . . . . 6 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → 𝑦tpos 𝐹𝑧)
63		df-br 5139	. . . . . 6 ⊢ (𝑦tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
64	62, 63	sylib 217	. . . . 5 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
65	64	exlimiv 1925	. . . 4 ⊢ (∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
66	16, 65	sylbi 216	. . 3 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
67	13, 66	relssi 5777	. 2 ⊢ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ tpos 𝐹
68	12, 67	eqssi 3990	1 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1533  ∃wex 1773   ∈ wcel 2098  Vcvv 3466   ∪ cun 3938   ⊆ wss 3940  ∅c0 4314  {csn 4620  ⟨cop 4626  ∪ cuni 4899   class class class wbr 5138   ↦ cmpt 5221   × cxp 5664  ^◡ccnv 5665  dom cdm 5666   ↾ cres 5668   ∘ ccom 5670  Rel wrel 5671  tpos ctpos 8205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-fv 6541  df-tpos 8206

This theorem is referenced by:  tposco  8237  nftpos  8241  oftpos  22264