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