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 { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )