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