This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝑥 ∈ { ∅ } → ( 𝑥 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 biimtrid ⊢ ( ¬ ∅ ∈ 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 𝐹 )