Theorem dftpos4 6493

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 6475	. . 3 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
2		relcnv 5139	. . . . . . 7 ⊢ Rel ◡dom 𝐹
3		df-rel 4755	. . . . . . 7 ⊢ (Rel ◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V))
4	2, 3	mpbi 145	. . . . . 6 ⊢ ◡dom 𝐹 ⊆ (V × V)
5		unss1 3387	. . . . . 6 ⊢ (◡dom 𝐹 ⊆ (V × V) → (◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}))
6		resmpt 5085	. . . . . 6 ⊢ ((◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}) → ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
7	4, 5, 6	mp2b 8	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})
8		resss 5061	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
9	7, 8	eqsstrri 3270	. . . 4 ⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
10		coss2 4910	. . . 4 ⊢ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) → (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})))
11	9, 10	ax-mp 5	. . 3 ⊢ (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
12	1, 11	eqsstri 3269	. 2 ⊢ tpos 𝐹 ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
13		relco 5260	. . 3 ⊢ Rel (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
14		vex 2815	. . . . 5 ⊢ 𝑦 ∈ V
15		vex 2815	. . . . 5 ⊢ 𝑧 ∈ V
16	14, 15	opelco 4926	. . . 4 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ↔ ∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧))
17		vex 2815	. . . . . . . . 9 ⊢ 𝑤 ∈ V
18		eleq1 2295	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ((V × V) ∪ {∅}) ↔ 𝑦 ∈ ((V × V) ∪ {∅})))
19		sneq 3699	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
20	19	cnveqd 4930	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ◡{𝑥} = ◡{𝑦})
21	20	unieqd 3924	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ∪ ◡{𝑥} = ∪ ◡{𝑦})
22	21	eqeq2d 2244	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑧 = ∪ ◡{𝑥} ↔ 𝑧 = ∪ ◡{𝑦}))
23	18, 22	anbi12d 473	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦})))
24		eqeq1 2239	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (𝑧 = ∪ ◡{𝑦} ↔ 𝑤 = ∪ ◡{𝑦}))
25	24	anbi2d 464	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → ((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦})))
26		df-mpt 4172	. . . . . . . . 9 ⊢ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥})}
27	14, 17, 23, 25, 26	brab 4390	. . . . . . . 8 ⊢ (𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}))
28		simplr 529	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 = ∪ ◡{𝑦})
29	17, 15	breldm 4959	. . . . . . . . . . . . 13 ⊢ (𝑤𝐹𝑧 → 𝑤 ∈ dom 𝐹)
30	29	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 ∈ dom 𝐹)
31	28, 30	eqeltrrd 2310	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦} ∈ dom 𝐹)
32		elvv 4811	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (V × V) ↔ ∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩)
33		opswapg 5248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V) → ∪ ◡{⟨𝑧, 𝑤⟩} = ⟨𝑤, 𝑧⟩)
34	15, 17, 33	mp2an 426	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ◡{⟨𝑧, 𝑤⟩} = ⟨𝑤, 𝑧⟩
35	34	eleq1i 2298	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
36	15, 17	opelcnv 4936	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
37	35, 36	bitr4i 187	. . . . . . . . . . . . . . . 16 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)
38		sneq 3699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → {𝑦} = {⟨𝑧, 𝑤⟩})
39	38	cnveqd 4930	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ◡{𝑦} = ◡{⟨𝑧, 𝑤⟩})
40	39	unieqd 3924	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ∪ ◡{𝑦} = ∪ ◡{⟨𝑧, 𝑤⟩})
41	40	eleq1d 2301	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ ∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹))
42		eleq1 2295	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ◡dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹))
43	41, 42	bibi12d 235	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ((∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹) ↔ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)))
44	37, 43	mpbiri 168	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
45	44	exlimivv 1946	. . . . . . . . . . . . . 14 ⊢ (∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
46	32, 45	sylbi 121	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (V × V) → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
47	46	biimpcd 159	. . . . . . . . . . . 12 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ ◡dom 𝐹))
48		elun1 3385	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ◡dom 𝐹 → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
49	47, 48	syl6 33	. . . . . . . . . . 11 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
50	31, 49	syl 14	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
51		elun2 3386	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
52	51	a1i 9	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
53		simpll 527	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ ((V × V) ∪ {∅}))
54		elun 3359	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((V × V) ∪ {∅}) ↔ (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
55	53, 54	sylib 122	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
56	50, 52, 55	mpjaod 726	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
57		simpr 110	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤𝐹𝑧)
58	28, 57	eqbrtrrd 4132	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦}𝐹𝑧)
59	56, 58	jca 306	. . . . . . . 8 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
60	27, 59	sylanb 284	. . . . . . 7 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
61		brtpos2 6481	. . . . . . . 8 ⊢ (𝑧 ∈ V → (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧)))
62	15, 61	ax-mp 5	. . . . . . 7 ⊢ (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
63	60, 62	sylibr 134	. . . . . 6 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → 𝑦tpos 𝐹𝑧)
64		df-br 4109	. . . . . 6 ⊢ (𝑦tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
65	63, 64	sylib 122	. . . . 5 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
66	65	exlimiv 1647	. . . 4 ⊢ (∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
67	16, 66	sylbi 121	. . 3 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
68	13, 67	relssi 4840	. 2 ⊢ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ tpos 𝐹
69	12, 68	eqssi 3253	1 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 716   = wceq 1398  ∃wex 1541   ∈ wcel 2203  Vcvv 2812   ∪ cun 3208   ⊆ wss 3210  ∅c0 3507  {csn 3688  ⟨cop 3691  ∪ cuni 3913   class class class wbr 4108   ↦ cmpt 4170   × cxp 4746  ^◡ccnv 4747  dom cdm 4748   ↾ cres 4750   ∘ ccom 4752  Rel wrel 4753  tpos ctpos 6474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321  ax-un 4553

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2814  df-sbc 3042  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-mpt 4172  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-iota 5311  df-fun 5353  df-fn 5354  df-fv 5359  df-tpos 6475

This theorem is referenced by:  tposco  6505  nftpos  6509