Metamath Proof Explorer


Theorem frsn

Description: Founded relation on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion frsn ( Rel 𝑅 → ( 𝑅 Fr { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 snprc ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
2 fr0 𝑅 Fr ∅
3 freq2 ( { 𝐴 } = ∅ → ( 𝑅 Fr { 𝐴 } ↔ 𝑅 Fr ∅ ) )
4 2 3 mpbiri ( { 𝐴 } = ∅ → 𝑅 Fr { 𝐴 } )
5 1 4 sylbi ( ¬ 𝐴 ∈ V → 𝑅 Fr { 𝐴 } )
6 5 adantl ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → 𝑅 Fr { 𝐴 } )
7 brrelex1 ( ( Rel 𝑅𝐴 𝑅 𝐴 ) → 𝐴 ∈ V )
8 7 stoic1a ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ¬ 𝐴 𝑅 𝐴 )
9 6 8 2thd ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ( 𝑅 Fr { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )
10 9 ex ( Rel 𝑅 → ( ¬ 𝐴 ∈ V → ( 𝑅 Fr { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) ) )
11 df-fr ( 𝑅 Fr { 𝐴 } ↔ ∀ 𝑥 ( ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) )
12 sssn ( 𝑥 ⊆ { 𝐴 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) )
13 neor ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ↔ ( 𝑥 ≠ ∅ → 𝑥 = { 𝐴 } ) )
14 12 13 sylbb ( 𝑥 ⊆ { 𝐴 } → ( 𝑥 ≠ ∅ → 𝑥 = { 𝐴 } ) )
15 14 imp ( ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) → 𝑥 = { 𝐴 } )
16 15 adantl ( ( 𝐴 ∈ V ∧ ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) ) → 𝑥 = { 𝐴 } )
17 eqimss ( 𝑥 = { 𝐴 } → 𝑥 ⊆ { 𝐴 } )
18 17 adantl ( ( 𝐴 ∈ V ∧ 𝑥 = { 𝐴 } ) → 𝑥 ⊆ { 𝐴 } )
19 snnzg ( 𝐴 ∈ V → { 𝐴 } ≠ ∅ )
20 neeq1 ( 𝑥 = { 𝐴 } → ( 𝑥 ≠ ∅ ↔ { 𝐴 } ≠ ∅ ) )
21 19 20 syl5ibrcom ( 𝐴 ∈ V → ( 𝑥 = { 𝐴 } → 𝑥 ≠ ∅ ) )
22 21 imp ( ( 𝐴 ∈ V ∧ 𝑥 = { 𝐴 } ) → 𝑥 ≠ ∅ )
23 18 22 jca ( ( 𝐴 ∈ V ∧ 𝑥 = { 𝐴 } ) → ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) )
24 16 23 impbida ( 𝐴 ∈ V → ( ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) ↔ 𝑥 = { 𝐴 } ) )
25 24 imbi1d ( 𝐴 ∈ V → ( ( ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) ↔ ( 𝑥 = { 𝐴 } → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) ) )
26 25 albidv ( 𝐴 ∈ V → ( ∀ 𝑥 ( ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 = { 𝐴 } → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) ) )
27 snex { 𝐴 } ∈ V
28 raleq ( 𝑥 = { 𝐴 } → ( ∀ 𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ↔ ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝑦 ) )
29 28 rexeqbi1dv ( 𝑥 = { 𝐴 } → ( ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ↔ ∃ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝑦 ) )
30 27 29 ceqsalv ( ∀ 𝑥 ( 𝑥 = { 𝐴 } → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) ↔ ∃ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝑦 )
31 26 30 bitrdi ( 𝐴 ∈ V → ( ∀ 𝑥 ( ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) ↔ ∃ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝑦 ) )
32 11 31 syl5bb ( 𝐴 ∈ V → ( 𝑅 Fr { 𝐴 } ↔ ∃ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝑦 ) )
33 breq2 ( 𝑦 = 𝐴 → ( 𝑧 𝑅 𝑦𝑧 𝑅 𝐴 ) )
34 33 notbid ( 𝑦 = 𝐴 → ( ¬ 𝑧 𝑅 𝑦 ↔ ¬ 𝑧 𝑅 𝐴 ) )
35 34 ralbidv ( 𝑦 = 𝐴 → ( ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝑦 ↔ ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝐴 ) )
36 35 rexsng ( 𝐴 ∈ V → ( ∃ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝑦 ↔ ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝐴 ) )
37 breq1 ( 𝑧 = 𝐴 → ( 𝑧 𝑅 𝐴𝐴 𝑅 𝐴 ) )
38 37 notbid ( 𝑧 = 𝐴 → ( ¬ 𝑧 𝑅 𝐴 ↔ ¬ 𝐴 𝑅 𝐴 ) )
39 38 ralsng ( 𝐴 ∈ V → ( ∀ 𝑧 ∈ { 𝐴 } ¬ 𝑧 𝑅 𝐴 ↔ ¬ 𝐴 𝑅 𝐴 ) )
40 32 36 39 3bitrd ( 𝐴 ∈ V → ( 𝑅 Fr { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )
41 10 40 pm2.61d2 ( Rel 𝑅 → ( 𝑅 Fr { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )