Theorem fneref

Description: Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009)

	Ref	Expression
Assertion	fneref	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 Fne 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐴 = ∪ 𝐴
2		ssid	⊢ 𝑥 ⊆ 𝑥
3		elequ2	⊢ ( 𝑧 = 𝑥 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑥 ) )
4		sseq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ⊆ 𝑥 ↔ 𝑥 ⊆ 𝑥 ) )
5	3 4	anbi12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑥 ) ) )
6	5	rspcev	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑥 ) ) → ∃ 𝑧 ∈ 𝐴 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
7	2 6	mpanr2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑧 ∈ 𝐴 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
8	7	rgen2	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐴 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 )
9	1 8	pm3.2i	⊢ ( ∪ 𝐴 = ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐴 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
10	1 1	isfne2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 Fne 𝐴 ↔ ( ∪ 𝐴 = ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐴 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) )
11	9 10	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 Fne 𝐴 )