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

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 bitrid ⊢ ( 𝐴 ∈ 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 { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )