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

Metamath Proof Explorer

Theorem bnj149

Description: Technical lemma for bnj151 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses bnj149.1 ⊢ ( 𝜃1 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
bnj149.2 ⊢ ( 𝜁0 ↔ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
bnj149.3 ⊢ ( 𝜁1 ↔ [ 𝑔 / 𝑓 ] 𝜁0 )
bnj149.4 ⊢ ( 𝜑1 ↔ [ 𝑔 / 𝑓 ] 𝜑′ )
bnj149.5 ⊢ ( 𝜓1 ↔ [ 𝑔 / 𝑓 ] 𝜓′ )
bnj149.6 ⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
Assertion bnj149 𝜃1

Proof

Step Hyp Ref Expression
1 bnj149.1 ⊢ ( 𝜃1 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
2 bnj149.2 ⊢ ( 𝜁0 ↔ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
3 bnj149.3 ⊢ ( 𝜁1 ↔ [ 𝑔 / 𝑓 ] 𝜁0 )
4 bnj149.4 ⊢ ( 𝜑1 ↔ [ 𝑔 / 𝑓 ] 𝜑′ )
5 bnj149.5 ⊢ ( 𝜓1 ↔ [ 𝑔 / 𝑓 ] 𝜓′ )
6 bnj149.6 ⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
7 simpr1 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝑓 Fn 1o )
8 df1o2 ⊢ 1o = { ∅ }
9 8 fneq2i ⊢ ( 𝑓 Fn 1o ↔ 𝑓 Fn { ∅ } )
10 7 9 sylib ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝑓 Fn { ∅ } )
11 simpr2 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝜑′ )
12 11 6 sylib ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
13 fvex ⊢ ( 𝑓 ‘ ∅ ) ∈ V
14 13 elsn ⊢ ( ( 𝑓 ‘ ∅ ) ∈ { pred ( 𝑥 , 𝐴 , 𝑅 ) } ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
15 12 14 sylibr ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → ( 𝑓 ‘ ∅ ) ∈ { pred ( 𝑥 , 𝐴 , 𝑅 ) } )
16 0ex ⊢ ∅ ∈ V
17 fveq2 ⊢ ( 𝑔 = ∅ → ( 𝑓 ‘ 𝑔 ) = ( 𝑓 ‘ ∅ ) )
18 17 eleq1d ⊢ ( 𝑔 = ∅ → ( ( 𝑓 ‘ 𝑔 ) ∈ { pred ( 𝑥 , 𝐴 , 𝑅 ) } ↔ ( 𝑓 ‘ ∅ ) ∈ { pred ( 𝑥 , 𝐴 , 𝑅 ) } ) )
19 16 18 ralsn ⊢ ( ∀ 𝑔 ∈ { ∅ } ( 𝑓 ‘ 𝑔 ) ∈ { pred ( 𝑥 , 𝐴 , 𝑅 ) } ↔ ( 𝑓 ‘ ∅ ) ∈ { pred ( 𝑥 , 𝐴 , 𝑅 ) } )
20 15 19 sylibr ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → ∀ 𝑔 ∈ { ∅ } ( 𝑓 ‘ 𝑔 ) ∈ { pred ( 𝑥 , 𝐴 , 𝑅 ) } )
21 ffnfv ⊢ ( 𝑓 : { ∅ } ⟶ { pred ( 𝑥 , 𝐴 , 𝑅 ) } ↔ ( 𝑓 Fn { ∅ } ∧ ∀ 𝑔 ∈ { ∅ } ( 𝑓 ‘ 𝑔 ) ∈ { pred ( 𝑥 , 𝐴 , 𝑅 ) } ) )
22 10 20 21 sylanbrc ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝑓 : { ∅ } ⟶ { pred ( 𝑥 , 𝐴 , 𝑅 ) } )
23 bnj93 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V )
24 23 adantr ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V )
25 fsng ⊢ ( ( ∅ ∈ V ∧ pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V ) → ( 𝑓 : { ∅ } ⟶ { pred ( 𝑥 , 𝐴 , 𝑅 ) } ↔ 𝑓 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ) )
26 16 24 25 sylancr ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → ( 𝑓 : { ∅ } ⟶ { pred ( 𝑥 , 𝐴 , 𝑅 ) } ↔ 𝑓 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ) )
27 22 26 mpbid ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝑓 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } )
28 27 ex ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) → 𝑓 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ) )
29 28 alrimiv ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑓 ( ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) → 𝑓 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ) )
30 mo2icl ⊢ ( ∀ 𝑓 ( ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) → 𝑓 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
31 29 30 syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
32 31 1 mpbir ⊢ 𝜃1