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 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 𝐹 )