finxpreclem2

Description: Lemma for ^^ recursion theorems. (Contributed by ML, 17-Oct-2020)

		Ref	Expression
	Assertion	finxpreclem2	⊢ ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ¬ ∅ = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑥 ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 )
2		nfmpo2	⊢ Ⅎ 𝑥 ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
3		nfcv	⊢ Ⅎ 𝑥 ⟨ 1_o , 𝑋 ⟩
4	2 3	nffv	⊢ Ⅎ 𝑥 ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ )
5		nfcv	⊢ Ⅎ 𝑥 ∅
6	4 5	nfne	⊢ Ⅎ 𝑥 ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅
7	1 6	nfim	⊢ Ⅎ 𝑥 ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ )
8		nfv	⊢ Ⅎ 𝑛 𝑥 = 𝑋
9		nfv	⊢ Ⅎ 𝑛 ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 )
10		nfmpo1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
11		nfcv	⊢ Ⅎ 𝑛 ⟨ 1_o , 𝑋 ⟩
12	10 11	nffv	⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ )
13		nfcv	⊢ Ⅎ 𝑛 ∅
14	12 13	nfne	⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅
15	9 14	nfim	⊢ Ⅎ 𝑛 ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ )
16	8 15	nfim	⊢ Ⅎ 𝑛 ( 𝑥 = 𝑋 → ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ ) )
17		1onn	⊢ 1_o ∈ ω
18	17	elexi	⊢ 1_o ∈ V
19		df-ov	⊢ ( 1_o ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) 𝑋 ) = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ )
20		0ex	⊢ ∅ ∈ V
21		opex	⊢ ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ ∈ V
22		opex	⊢ ⟨ 𝑛 , 𝑥 ⟩ ∈ V
23	21 22	ifex	⊢ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ∈ V
24	20 23	ifex	⊢ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ∈ V
25	24	csbex	⊢ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ∈ V
26	25	csbex	⊢ ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ∈ V
27		eqid	⊢ ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
28	27	ovmpos	⊢ ( ( 1_o ∈ ω ∧ 𝑋 ∈ V ∧ ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ∈ V ) → ( 1_o ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) 𝑋 ) = ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
29	17 26 28	mp3an13	⊢ ( 𝑋 ∈ V → ( 1_o ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) 𝑋 ) = ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
30	29	adantr	⊢ ( ( 𝑋 ∈ V ∧ ( ¬ 𝑋 ∈ 𝑈 ∧ ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ) ) → ( 1_o ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) 𝑋 ) = ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
31		csbeq1a	⊢ ( 𝑥 = 𝑋 → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
32		csbeq1a	⊢ ( 𝑛 = 1_o → ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
33	31 32	sylan9eqr	⊢ ( ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
34	33	adantl	⊢ ( ( ¬ 𝑋 ∈ 𝑈 ∧ ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
35		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
36	35	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑥 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈 ) )
37	36	biimprcd	⊢ ( ¬ 𝑋 ∈ 𝑈 → ( 𝑥 = 𝑋 → ¬ 𝑥 ∈ 𝑈 ) )
38		pm3.14	⊢ ( ( ¬ 𝑛 = 1_o ∨ ¬ 𝑥 ∈ 𝑈 ) → ¬ ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) )
39	38	olcs	⊢ ( ¬ 𝑥 ∈ 𝑈 → ¬ ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) )
40	37 39	syl6	⊢ ( ¬ 𝑋 ∈ 𝑈 → ( 𝑥 = 𝑋 → ¬ ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) ) )
41		iffalse	⊢ ( ¬ ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) )
42	40 41	syl6	⊢ ( ¬ 𝑋 ∈ 𝑈 → ( 𝑥 = 𝑋 → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
43	42	imp	⊢ ( ( ¬ 𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋 ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) )
44		ifeqor	⊢ ( if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ ∨ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ )
45		vuniex	⊢ ∪ 𝑛 ∈ V
46		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
47	45 46	opnzi	⊢ ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ ≠ ∅
48	47	neii	⊢ ¬ ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ = ∅
49		eqeq1	⊢ ( if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ → ( if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ∅ ↔ ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ = ∅ ) )
50	48 49	mtbiri	⊢ ( if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ → ¬ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ∅ )
51		vex	⊢ 𝑛 ∈ V
52		vex	⊢ 𝑥 ∈ V
53	51 52	opnzi	⊢ ⟨ 𝑛 , 𝑥 ⟩ ≠ ∅
54	53	neii	⊢ ¬ ⟨ 𝑛 , 𝑥 ⟩ = ∅
55		eqeq1	⊢ ( if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ → ( if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ∅ ↔ ⟨ 𝑛 , 𝑥 ⟩ = ∅ ) )
56	54 55	mtbiri	⊢ ( if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ → ¬ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ∅ )
57	50 56	jaoi	⊢ ( ( if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ ∨ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ ) → ¬ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ∅ )
58	44 57	mp1i	⊢ ( ( ¬ 𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋 ) → ¬ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ∅ )
59	58	neqned	⊢ ( ( ¬ 𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ≠ ∅ )
60	43 59	eqnetrd	⊢ ( ( ¬ 𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋 ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ≠ ∅ )
61	60	adantrl	⊢ ( ( ¬ 𝑋 ∈ 𝑈 ∧ ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ≠ ∅ )
62	34 61	eqnetrrd	⊢ ( ( ¬ 𝑋 ∈ 𝑈 ∧ ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ) → ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ≠ ∅ )
63	62	adantl	⊢ ( ( 𝑋 ∈ V ∧ ( ¬ 𝑋 ∈ 𝑈 ∧ ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ) ) → ⦋ 1_o / 𝑛 ⦌ ⦋ 𝑋 / 𝑥 ⦌ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ≠ ∅ )
64	30 63	eqnetrd	⊢ ( ( 𝑋 ∈ V ∧ ( ¬ 𝑋 ∈ 𝑈 ∧ ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ) ) → ( 1_o ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) 𝑋 ) ≠ ∅ )
65	19 64	eqnetrrid	⊢ ( ( 𝑋 ∈ V ∧ ( ¬ 𝑋 ∈ 𝑈 ∧ ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ) ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ )
66	65	ancom2s	⊢ ( ( 𝑋 ∈ V ∧ ( ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ∧ ¬ 𝑋 ∈ 𝑈 ) ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ )
67	66	an12s	⊢ ( ( ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ∧ ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ )
68	67	exp31	⊢ ( 𝑛 = 1_o → ( 𝑥 = 𝑋 → ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ ) ) )
69	16 18 68	vtoclef	⊢ ( 𝑥 = 𝑋 → ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ ) )
70	7 69	vtoclefex	⊢ ( 𝑋 ∈ V → ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ ) )
71	70	anabsi5	⊢ ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) ≠ ∅ )
72	71	necomd	⊢ ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ∅ ≠ ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) )
73	72	neneqd	⊢ ( ( 𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈 ) → ¬ ∅ = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) )

Metamath Proof Explorer

Theorem finxpreclem2

Proof