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

Metamath Proof Explorer

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