Theorem reldmtpos 8275

Description: Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)

Assertion

Ref	Expression
reldmtpos	⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹)

Proof of Theorem reldmtpos

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 5325	. . . . 5 ⊢ ∅ ∈ V
2	1	eldm 5925	. . . 4 ⊢ (∅ ∈ dom 𝐹 ↔ ∃𝑦∅𝐹𝑦)
3		brtpos0 8274	. . . . . . 7 ⊢ (𝑦 ∈ V → (∅tpos 𝐹𝑦 ↔ ∅𝐹𝑦))
4	3	elv 3493	. . . . . 6 ⊢ (∅tpos 𝐹𝑦 ↔ ∅𝐹𝑦)
5		0nelrel0 5760	. . . . . . 7 ⊢ (Rel dom tpos 𝐹 → ¬ ∅ ∈ dom tpos 𝐹)
6		vex 3492	. . . . . . . 8 ⊢ 𝑦 ∈ V
7	1, 6	breldm 5933	. . . . . . 7 ⊢ (∅tpos 𝐹𝑦 → ∅ ∈ dom tpos 𝐹)
8	5, 7	nsyl3 138	. . . . . 6 ⊢ (∅tpos 𝐹𝑦 → ¬ Rel dom tpos 𝐹)
9	4, 8	sylbir 235	. . . . 5 ⊢ (∅𝐹𝑦 → ¬ Rel dom tpos 𝐹)
10	9	exlimiv 1929	. . . 4 ⊢ (∃𝑦∅𝐹𝑦 → ¬ Rel dom tpos 𝐹)
11	2, 10	sylbi 217	. . 3 ⊢ (∅ ∈ dom 𝐹 → ¬ Rel dom tpos 𝐹)
12	11	con2i 139	. 2 ⊢ (Rel dom tpos 𝐹 → ¬ ∅ ∈ dom 𝐹)
13		vex 3492	. . . . . 6 ⊢ 𝑥 ∈ V
14	13	eldm 5925	. . . . 5 ⊢ (𝑥 ∈ dom tpos 𝐹 ↔ ∃𝑦 𝑥tpos 𝐹𝑦)
15		relcnv 6134	. . . . . . . . . . 11 ⊢ Rel ◡dom 𝐹
16		df-rel 5707	. . . . . . . . . . 11 ⊢ (Rel ◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V))
17	15, 16	mpbi 230	. . . . . . . . . 10 ⊢ ◡dom 𝐹 ⊆ (V × V)
18	17	sseli 4004	. . . . . . . . 9 ⊢ (𝑥 ∈ ◡dom 𝐹 → 𝑥 ∈ (V × V))
19	18	a1i 11	. . . . . . . 8 ⊢ ((¬ ∅ ∈ dom 𝐹 ∧ 𝑥tpos 𝐹𝑦) → (𝑥 ∈ ◡dom 𝐹 → 𝑥 ∈ (V × V)))
20		elsni 4665	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {∅} → 𝑥 = ∅)
21	20	breq1d 5176	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {∅} → (𝑥tpos 𝐹𝑦 ↔ ∅tpos 𝐹𝑦))
22	1, 6	breldm 5933	. . . . . . . . . . . . 13 ⊢ (∅𝐹𝑦 → ∅ ∈ dom 𝐹)
23	22	pm2.24d 151	. . . . . . . . . . . 12 ⊢ (∅𝐹𝑦 → (¬ ∅ ∈ dom 𝐹 → 𝑥 ∈ (V × V)))
24	4, 23	sylbi 217	. . . . . . . . . . 11 ⊢ (∅tpos 𝐹𝑦 → (¬ ∅ ∈ dom 𝐹 → 𝑥 ∈ (V × V)))
25	21, 24	biimtrdi 253	. . . . . . . . . 10 ⊢ (𝑥 ∈ {∅} → (𝑥tpos 𝐹𝑦 → (¬ ∅ ∈ dom 𝐹 → 𝑥 ∈ (V × V))))
26	25	com3l 89	. . . . . . . . 9 ⊢ (𝑥tpos 𝐹𝑦 → (¬ ∅ ∈ dom 𝐹 → (𝑥 ∈ {∅} → 𝑥 ∈ (V × V))))
27	26	impcom 407	. . . . . . . 8 ⊢ ((¬ ∅ ∈ dom 𝐹 ∧ 𝑥tpos 𝐹𝑦) → (𝑥 ∈ {∅} → 𝑥 ∈ (V × V)))
28		brtpos2 8273	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ V → (𝑥tpos 𝐹𝑦 ↔ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑥}𝐹𝑦)))
29	6, 28	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑥tpos 𝐹𝑦 ↔ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑥}𝐹𝑦))
30	29	simplbi 497	. . . . . . . . . 10 ⊢ (𝑥tpos 𝐹𝑦 → 𝑥 ∈ (◡dom 𝐹 ∪ {∅}))
31		elun 4176	. . . . . . . . . 10 ⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↔ (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅}))
32	30, 31	sylib 218	. . . . . . . . 9 ⊢ (𝑥tpos 𝐹𝑦 → (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅}))
33	32	adantl 481	. . . . . . . 8 ⊢ ((¬ ∅ ∈ dom 𝐹 ∧ 𝑥tpos 𝐹𝑦) → (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅}))
34	19, 27, 33	mpjaod 859	. . . . . . 7 ⊢ ((¬ ∅ ∈ dom 𝐹 ∧ 𝑥tpos 𝐹𝑦) → 𝑥 ∈ (V × V))
35	34	ex 412	. . . . . 6 ⊢ (¬ ∅ ∈ dom 𝐹 → (𝑥tpos 𝐹𝑦 → 𝑥 ∈ (V × V)))
36	35	exlimdv 1932	. . . . 5 ⊢ (¬ ∅ ∈ dom 𝐹 → (∃𝑦 𝑥tpos 𝐹𝑦 → 𝑥 ∈ (V × V)))
37	14, 36	biimtrid 242	. . . 4 ⊢ (¬ ∅ ∈ dom 𝐹 → (𝑥 ∈ dom tpos 𝐹 → 𝑥 ∈ (V × V)))
38	37	ssrdv 4014	. . 3 ⊢ (¬ ∅ ∈ dom 𝐹 → dom tpos 𝐹 ⊆ (V × V))
39		df-rel 5707	. . 3 ⊢ (Rel dom tpos 𝐹 ↔ dom tpos 𝐹 ⊆ (V × V))
40	38, 39	sylibr 234	. 2 ⊢ (¬ ∅ ∈ dom 𝐹 → Rel dom tpos 𝐹)
41	12, 40	impbii 209	1 ⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846  ∃wex 1777   ∈ wcel 2108  Vcvv 3488   ∪ cun 3974   ⊆ wss 3976  ∅c0 4352  {csn 4648  ∪ cuni 4931   class class class wbr 5166   × cxp 5698  ^◡ccnv 5699  dom cdm 5700  Rel wrel 5705  tpos ctpos 8266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-fv 6581  df-tpos 8267

This theorem is referenced by:  dmtpos  8279