Theorem reldmtpos

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

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

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2	1	eldm	⊢ ( ∅ ∈ dom 𝐹 ↔ ∃ 𝑦 ∅ 𝐹 𝑦 )
3		brtpos0	⊢ ( 𝑦 ∈ V → ( ∅ tpos 𝐹 𝑦 ↔ ∅ 𝐹 𝑦 ) )
4	3	elv	⊢ ( ∅ tpos 𝐹 𝑦 ↔ ∅ 𝐹 𝑦 )
5		0nelrel0	⊢ ( Rel dom tpos 𝐹 → ¬ ∅ ∈ dom tpos 𝐹 )
6		vex	⊢ 𝑦 ∈ V
7	1 6	breldm	⊢ ( ∅ tpos 𝐹 𝑦 → ∅ ∈ dom tpos 𝐹 )
8	5 7	nsyl3	⊢ ( ∅ tpos 𝐹 𝑦 → ¬ Rel dom tpos 𝐹 )
9	4 8	sylbir	⊢ ( ∅ 𝐹 𝑦 → ¬ Rel dom tpos 𝐹 )
10	9	exlimiv	⊢ ( ∃ 𝑦 ∅ 𝐹 𝑦 → ¬ Rel dom tpos 𝐹 )
11	2 10	sylbi	⊢ ( ∅ ∈ dom 𝐹 → ¬ Rel dom tpos 𝐹 )
12	11	con2i	⊢ ( Rel dom tpos 𝐹 → ¬ ∅ ∈ dom 𝐹 )
13		vex	⊢ 𝑥 ∈ V
14	13	eldm	⊢ ( 𝑥 ∈ dom tpos 𝐹 ↔ ∃ 𝑦 𝑥 tpos 𝐹 𝑦 )
15		relcnv	⊢ Rel ◡ dom 𝐹
16		df-rel	⊢ ( Rel ◡ dom 𝐹 ↔ ◡ dom 𝐹 ⊆ ( V × V ) )
17	15 16	mpbi	⊢ ◡ dom 𝐹 ⊆ ( V × V )
18	17	sseli	⊢ ( 𝑥 ∈ ◡ dom 𝐹 → 𝑥 ∈ ( V × V ) )
19	18	a1i	⊢ ( ( ¬ ∅ ∈ dom 𝐹 ∧ 𝑥 tpos 𝐹 𝑦 ) → ( 𝑥 ∈ ◡ dom 𝐹 → 𝑥 ∈ ( V × V ) ) )
20		elsni	⊢ ( 𝑥 ∈ { ∅ } → 𝑥 = ∅ )
21	20	breq1d	⊢ ( 𝑥 ∈ { ∅ } → ( 𝑥 tpos 𝐹 𝑦 ↔ ∅ tpos 𝐹 𝑦 ) )
22	1 6	breldm	⊢ ( ∅ 𝐹 𝑦 → ∅ ∈ dom 𝐹 )
23	22	pm2.24d	⊢ ( ∅ 𝐹 𝑦 → ( ¬ ∅ ∈ dom 𝐹 → 𝑥 ∈ ( V × V ) ) )
24	4 23	sylbi	⊢ ( ∅ tpos 𝐹 𝑦 → ( ¬ ∅ ∈ dom 𝐹 → 𝑥 ∈ ( V × V ) ) )
25	21 24	syl6bi	⊢ ( 𝑥 ∈ { ∅ } → ( 𝑥 tpos 𝐹 𝑦 → ( ¬ ∅ ∈ dom 𝐹 → 𝑥 ∈ ( V × V ) ) ) )
26	25	com3l	⊢ ( 𝑥 tpos 𝐹 𝑦 → ( ¬ ∅ ∈ dom 𝐹 → ( 𝑥 ∈ { ∅ } → 𝑥 ∈ ( V × V ) ) ) )
27	26	impcom	⊢ ( ( ¬ ∅ ∈ dom 𝐹 ∧ 𝑥 tpos 𝐹 𝑦 ) → ( 𝑥 ∈ { ∅ } → 𝑥 ∈ ( V × V ) ) )
28		brtpos2	⊢ ( 𝑦 ∈ V → ( 𝑥 tpos 𝐹 𝑦 ↔ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑥 } 𝐹 𝑦 ) ) )
29	6 28	ax-mp	⊢ ( 𝑥 tpos 𝐹 𝑦 ↔ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑥 } 𝐹 𝑦 ) )
30	29	simplbi	⊢ ( 𝑥 tpos 𝐹 𝑦 → 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) )
31		elun	⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↔ ( 𝑥 ∈ ◡ dom 𝐹 ∨ 𝑥 ∈ { ∅ } ) )
32	30 31	sylib	⊢ ( 𝑥 tpos 𝐹 𝑦 → ( 𝑥 ∈ ◡ dom 𝐹 ∨ 𝑥 ∈ { ∅ } ) )
33	32	adantl	⊢ ( ( ¬ ∅ ∈ dom 𝐹 ∧ 𝑥 tpos 𝐹 𝑦 ) → ( 𝑥 ∈ ◡ dom 𝐹 ∨ 𝑥 ∈ { ∅ } ) )
34	19 27 33	mpjaod	⊢ ( ( ¬ ∅ ∈ dom 𝐹 ∧ 𝑥 tpos 𝐹 𝑦 ) → 𝑥 ∈ ( V × V ) )
35	34	ex	⊢ ( ¬ ∅ ∈ dom 𝐹 → ( 𝑥 tpos 𝐹 𝑦 → 𝑥 ∈ ( V × V ) ) )
36	35	exlimdv	⊢ ( ¬ ∅ ∈ dom 𝐹 → ( ∃ 𝑦 𝑥 tpos 𝐹 𝑦 → 𝑥 ∈ ( V × V ) ) )
37	14 36	syl5bi	⊢ ( ¬ ∅ ∈ dom 𝐹 → ( 𝑥 ∈ dom tpos 𝐹 → 𝑥 ∈ ( V × V ) ) )
38	37	ssrdv	⊢ ( ¬ ∅ ∈ dom 𝐹 → dom tpos 𝐹 ⊆ ( V × V ) )
39		df-rel	⊢ ( Rel dom tpos 𝐹 ↔ dom tpos 𝐹 ⊆ ( V × V ) )
40	38 39	sylibr	⊢ ( ¬ ∅ ∈ dom 𝐹 → Rel dom tpos 𝐹 )
41	12 40	impbii	⊢ ( Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹 )