finixpnum

Description: A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019)

		Ref	Expression
	Assertion	finixpnum	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ dom card ) → X 𝑥 ∈ 𝐴 𝐵 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		raleq	⊢ ( 𝑤 = ∅ → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀ 𝑥 ∈ ∅ 𝐵 ∈ dom card ) )
2		ixpeq1	⊢ ( 𝑤 = ∅ → X 𝑥 ∈ 𝑤 𝐵 = X 𝑥 ∈ ∅ 𝐵 )
3		ixp0x	⊢ X 𝑥 ∈ ∅ 𝐵 = { ∅ }
4	2 3	eqtrdi	⊢ ( 𝑤 = ∅ → X 𝑥 ∈ 𝑤 𝐵 = { ∅ } )
5	4	eleq1d	⊢ ( 𝑤 = ∅ → ( X 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ { ∅ } ∈ dom card ) )
6	1 5	imbi12d	⊢ ( 𝑤 = ∅ → ( ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card → X 𝑥 ∈ 𝑤 𝐵 ∈ dom card ) ↔ ( ∀ 𝑥 ∈ ∅ 𝐵 ∈ dom card → { ∅ } ∈ dom card ) ) )
7		raleq	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) )
8		ixpeq1	⊢ ( 𝑤 = 𝑦 → X 𝑥 ∈ 𝑤 𝐵 = X 𝑥 ∈ 𝑦 𝐵 )
9	8	eleq1d	⊢ ( 𝑤 = 𝑦 → ( X 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) )
10	7 9	imbi12d	⊢ ( 𝑤 = 𝑦 → ( ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card → X 𝑥 ∈ 𝑤 𝐵 ∈ dom card ) ↔ ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) ) )
11		raleq	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) )
12		ralunb	⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ↔ ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ∀ 𝑥 ∈ { 𝑧 } 𝐵 ∈ dom card ) )
13		vex	⊢ 𝑧 ∈ V
14		ralsnsg	⊢ ( 𝑧 ∈ V → ( ∀ 𝑥 ∈ { 𝑧 } 𝐵 ∈ dom card ↔ [ 𝑧 / 𝑥 ] 𝐵 ∈ dom card ) )
15		sbcel1g	⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑥 ] 𝐵 ∈ dom card ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) )
16	14 15	bitrd	⊢ ( 𝑧 ∈ V → ( ∀ 𝑥 ∈ { 𝑧 } 𝐵 ∈ dom card ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) )
17	13 16	ax-mp	⊢ ( ∀ 𝑥 ∈ { 𝑧 } 𝐵 ∈ dom card ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card )
18	17	anbi2i	⊢ ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ∀ 𝑥 ∈ { 𝑧 } 𝐵 ∈ dom card ) ↔ ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) )
19	12 18	bitri	⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ↔ ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) )
20	11 19	bitrdi	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) ) )
21		ixpeq1	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → X 𝑥 ∈ 𝑤 𝐵 = X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
22	21	eleq1d	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( X 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) )
23	20 22	imbi12d	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card → X 𝑥 ∈ 𝑤 𝐵 ∈ dom card ) ↔ ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) ) )
24		raleq	⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ dom card ) )
25		ixpeq1	⊢ ( 𝑤 = 𝐴 → X 𝑥 ∈ 𝑤 𝐵 = X 𝑥 ∈ 𝐴 𝐵 )
26	25	eleq1d	⊢ ( 𝑤 = 𝐴 → ( X 𝑥 ∈ 𝑤 𝐵 ∈ dom card ↔ X 𝑥 ∈ 𝐴 𝐵 ∈ dom card ) )
27	24 26	imbi12d	⊢ ( 𝑤 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ dom card → X 𝑥 ∈ 𝑤 𝐵 ∈ dom card ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ dom card → X 𝑥 ∈ 𝐴 𝐵 ∈ dom card ) ) )
28		snfi	⊢ { ∅ } ∈ Fin
29		finnum	⊢ ( { ∅ } ∈ Fin → { ∅ } ∈ dom card )
30	28 29	mp1i	⊢ ( ∀ 𝑥 ∈ ∅ 𝐵 ∈ dom card → { ∅ } ∈ dom card )
31		pm2.27	⊢ ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) → X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) )
32		xpnum	⊢ ( ( X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) → ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ dom card )
33	32	ancoms	⊢ ( ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ∧ X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) → ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ dom card )
34		xp1st	⊢ ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ( 1^st ‘ 𝑤 ) ∈ X 𝑥 ∈ 𝑦 𝐵 )
35		ixpfn	⊢ ( ( 1^st ‘ 𝑤 ) ∈ X 𝑥 ∈ 𝑦 𝐵 → ( 1^st ‘ 𝑤 ) Fn 𝑦 )
36	34 35	syl	⊢ ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ( 1^st ‘ 𝑤 ) Fn 𝑦 )
37		fvex	⊢ ( 2^nd ‘ 𝑤 ) ∈ V
38	13 37	fnsn	⊢ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } Fn { 𝑧 }
39	36 38	jctir	⊢ ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } Fn { 𝑧 } ) )
40		disjsn	⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
41	40	biimpri	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
42		fnun	⊢ ( ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } Fn { 𝑧 } ) ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) → ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) )
43	39 41 42	syl2anr	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) )
44		fvex	⊢ ( 1^st ‘ 𝑤 ) ∈ V
45	44	elixp	⊢ ( ( 1^st ‘ 𝑤 ) ∈ X 𝑥 ∈ 𝑦 𝐵 ↔ ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ∈ 𝐵 ) )
46	34 45	sylib	⊢ ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ∈ 𝐵 ) )
47		fvun1	⊢ ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } Fn { 𝑧 } ∧ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ∧ 𝑥 ∈ 𝑦 ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) )
48	38 47	mp3an2	⊢ ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ∧ 𝑥 ∈ 𝑦 ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) )
49	48	anassrs	⊢ ( ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) )
50	49	eleq1d	⊢ ( ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ↔ ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ∈ 𝐵 ) )
51	50	biimprd	⊢ ( ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ∈ 𝐵 → ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ) )
52	51	ralimdva	⊢ ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) → ( ∀ 𝑥 ∈ 𝑦 ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝑦 ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ) )
53	52	ancoms	⊢ ( ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ∧ ( 1^st ‘ 𝑤 ) Fn 𝑦 ) → ( ∀ 𝑥 ∈ 𝑦 ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝑦 ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ) )
54	53	impr	⊢ ( ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ∧ ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝑦 ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 )
55	41 46 54	syl2an	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ 𝑦 ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 )
56		vsnid	⊢ 𝑧 ∈ { 𝑧 }
57	41 56	jctir	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ∧ 𝑧 ∈ { 𝑧 } ) )
58		fvun2	⊢ ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } Fn { 𝑧 } ∧ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ∧ 𝑧 ∈ { 𝑧 } ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ 𝑧 ) )
59	38 58	mp3an2	⊢ ( ( ( 1^st ‘ 𝑤 ) Fn 𝑦 ∧ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ∧ 𝑧 ∈ { 𝑧 } ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ 𝑧 ) )
60	36 57 59	syl2anr	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ 𝑧 ) )
61		csbfv	⊢ ⦋ 𝑧 / 𝑥 ⦌ ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) = ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑧 )
62	13 37	fvsn	⊢ ( { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ 𝑧 ) = ( 2^nd ‘ 𝑤 )
63	62	eqcomi	⊢ ( 2^nd ‘ 𝑤 ) = ( { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ‘ 𝑧 )
64	60 61 63	3eqtr4g	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ⦋ 𝑧 / 𝑥 ⦌ ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) = ( 2^nd ‘ 𝑤 ) )
65		xp2nd	⊢ ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ( 2^nd ‘ 𝑤 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
66	65	adantl	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ( 2^nd ‘ 𝑤 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
67	64 66	eqeltrd	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ⦋ 𝑧 / 𝑥 ⦌ ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
68		ralsnsg	⊢ ( 𝑧 ∈ V → ( ∀ 𝑥 ∈ { 𝑧 } ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ↔ [ 𝑧 / 𝑥 ] ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ) )
69	13 68	ax-mp	⊢ ( ∀ 𝑥 ∈ { 𝑧 } ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ↔ [ 𝑧 / 𝑥 ] ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 )
70		sbcel12	⊢ ( [ 𝑧 / 𝑥 ] ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ↔ ⦋ 𝑧 / 𝑥 ⦌ ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
71	69 70	bitri	⊢ ( ∀ 𝑥 ∈ { 𝑧 } ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ↔ ⦋ 𝑧 / 𝑥 ⦌ ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
72	67 71	sylibr	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ { 𝑧 } ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 )
73		ralun	⊢ ( ( ∀ 𝑥 ∈ 𝑦 ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ { 𝑧 } ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 )
74	55 72 73	syl2anc	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 )
75		snex	⊢ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ∈ V
76	44 75	unex	⊢ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ∈ V
77	76	elixp	⊢ ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↔ ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ‘ 𝑥 ) ∈ 𝐵 ) )
78	43 74 77	sylanbrc	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) → ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
79	78	fmpttd	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) : ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
80		ixpfn	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → 𝑢 Fn ( 𝑦 ∪ { 𝑧 } ) )
81		ssun1	⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
82		fnssres	⊢ ( ( 𝑢 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑢 ↾ 𝑦 ) Fn 𝑦 )
83	80 81 82	sylancl	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → ( 𝑢 ↾ 𝑦 ) Fn 𝑦 )
84		vex	⊢ 𝑢 ∈ V
85	84	elixp	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↔ ( 𝑢 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 ) )
86		ssralv	⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝑦 ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 ) )
87	81 86	ax-mp	⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝑦 ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 )
88		fvres	⊢ ( 𝑥 ∈ 𝑦 → ( ( 𝑢 ↾ 𝑦 ) ‘ 𝑥 ) = ( 𝑢 ‘ 𝑥 ) )
89	88	eleq1d	⊢ ( 𝑥 ∈ 𝑦 → ( ( ( 𝑢 ↾ 𝑦 ) ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 ) )
90	89	biimprd	⊢ ( 𝑥 ∈ 𝑦 → ( ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 → ( ( 𝑢 ↾ 𝑦 ) ‘ 𝑥 ) ∈ 𝐵 ) )
91	90	ralimia	⊢ ( ∀ 𝑥 ∈ 𝑦 ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝑦 ( ( 𝑢 ↾ 𝑦 ) ‘ 𝑥 ) ∈ 𝐵 )
92	87 91	syl	⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝑦 ( ( 𝑢 ↾ 𝑦 ) ‘ 𝑥 ) ∈ 𝐵 )
93	92	adantl	⊢ ( ( 𝑢 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑢 ‘ 𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝑦 ( ( 𝑢 ↾ 𝑦 ) ‘ 𝑥 ) ∈ 𝐵 )
94	85 93	sylbi	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → ∀ 𝑥 ∈ 𝑦 ( ( 𝑢 ↾ 𝑦 ) ‘ 𝑥 ) ∈ 𝐵 )
95	84	resex	⊢ ( 𝑢 ↾ 𝑦 ) ∈ V
96	95	elixp	⊢ ( ( 𝑢 ↾ 𝑦 ) ∈ X 𝑥 ∈ 𝑦 𝐵 ↔ ( ( 𝑢 ↾ 𝑦 ) Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 𝑢 ↾ 𝑦 ) ‘ 𝑥 ) ∈ 𝐵 ) )
97	83 94 96	sylanbrc	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → ( 𝑢 ↾ 𝑦 ) ∈ X 𝑥 ∈ 𝑦 𝐵 )
98		ssun2	⊢ { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } )
99	98 56	sselii	⊢ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } )
100		csbeq1	⊢ ( 𝑤 = 𝑧 → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
101	100	fvixp	⊢ ( ( 𝑢 ∈ X 𝑤 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∧ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑢 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
102	99 101	mpan2	⊢ ( 𝑢 ∈ X 𝑤 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑤 / 𝑥 ⦌ 𝐵 → ( 𝑢 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
103		nfcv	⊢ Ⅎ 𝑤 𝐵
104		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐵
105		csbeq1a	⊢ ( 𝑥 = 𝑤 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
106	103 104 105	cbvixp	⊢ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = X 𝑤 ∈ ( 𝑦 ∪ { 𝑧 } ) ⦋ 𝑤 / 𝑥 ⦌ 𝐵
107	102 106	eleq2s	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → ( 𝑢 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
108		opelxpi	⊢ ( ( ( 𝑢 ↾ 𝑦 ) ∈ X 𝑥 ∈ 𝑦 𝐵 ∧ ( 𝑢 ‘ 𝑧 ) ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
109	97 107 108	syl2anc	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
110	109	adantl	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
111		disj3	⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ 𝑦 = ( 𝑦 ∖ { 𝑧 } ) )
112	40 111	sylbb1	⊢ ( ¬ 𝑧 ∈ 𝑦 → 𝑦 = ( 𝑦 ∖ { 𝑧 } ) )
113		difun2	⊢ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑧 } ) = ( 𝑦 ∖ { 𝑧 } )
114	112 113	eqtr4di	⊢ ( ¬ 𝑧 ∈ 𝑦 → 𝑦 = ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑧 } ) )
115	114	reseq2d	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝑢 ↾ 𝑦 ) = ( 𝑢 ↾ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑧 } ) ) )
116	115	uneq1d	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝑢 ↾ 𝑦 ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) = ( ( 𝑢 ↾ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑧 } ) ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
117	116	adantr	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( ( 𝑢 ↾ 𝑦 ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) = ( ( 𝑢 ↾ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑧 } ) ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
118		fvex	⊢ ( 𝑢 ‘ 𝑧 ) ∈ V
119	95 118	op1std	⊢ ( 𝑤 = ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ → ( 1^st ‘ 𝑤 ) = ( 𝑢 ↾ 𝑦 ) )
120	95 118	op2ndd	⊢ ( 𝑤 = ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ → ( 2^nd ‘ 𝑤 ) = ( 𝑢 ‘ 𝑧 ) )
121	120	opeq2d	⊢ ( 𝑤 = ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ → ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ = ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ )
122	121	sneqd	⊢ ( 𝑤 = ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ → { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } = { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } )
123	119 122	uneq12d	⊢ ( 𝑤 = ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ → ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) = ( ( 𝑢 ↾ 𝑦 ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
124		eqid	⊢ ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) = ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) )
125		snex	⊢ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ∈ V
126	95 125	unex	⊢ ( ( 𝑢 ↾ 𝑦 ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) ∈ V
127	123 124 126	fvmpt	⊢ ( ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ) = ( ( 𝑢 ↾ 𝑦 ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
128	109 127	syl	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ) = ( ( 𝑢 ↾ 𝑦 ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
129	128	adantl	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ) = ( ( 𝑢 ↾ 𝑦 ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
130		fnsnsplit	⊢ ( ( 𝑢 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑢 = ( ( 𝑢 ↾ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑧 } ) ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
131	80 99 130	sylancl	⊢ ( 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 → 𝑢 = ( ( 𝑢 ↾ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑧 } ) ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
132	131	adantl	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → 𝑢 = ( ( 𝑢 ↾ ( ( 𝑦 ∪ { 𝑧 } ) ∖ { 𝑧 } ) ) ∪ { ⟨ 𝑧 , ( 𝑢 ‘ 𝑧 ) ⟩ } ) )
133	117 129 132	3eqtr4rd	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → 𝑢 = ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ) )
134		fveq2	⊢ ( 𝑣 = ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ → ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ 𝑣 ) = ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ) )
135	134	rspceeqv	⊢ ( ( ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑢 = ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ ⟨ ( 𝑢 ↾ 𝑦 ) , ( 𝑢 ‘ 𝑧 ) ⟩ ) ) → ∃ 𝑣 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) 𝑢 = ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ 𝑣 ) )
136	110 133 135	syl2anc	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → ∃ 𝑣 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) 𝑢 = ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ 𝑣 ) )
137	136	ralrimiva	⊢ ( ¬ 𝑧 ∈ 𝑦 → ∀ 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∃ 𝑣 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) 𝑢 = ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ 𝑣 ) )
138		dffo3	⊢ ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) : ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) –onto→ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↔ ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) : ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∧ ∀ 𝑢 ∈ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∃ 𝑣 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) 𝑢 = ( ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) ‘ 𝑣 ) ) )
139	79 137 138	sylanbrc	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) : ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) –onto→ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
140		fonum	⊢ ( ( ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ dom card ∧ ( 𝑤 ∈ ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ( ( 1^st ‘ 𝑤 ) ∪ { ⟨ 𝑧 , ( 2^nd ‘ 𝑤 ) ⟩ } ) ) : ( X 𝑥 ∈ 𝑦 𝐵 × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) –onto→ X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card )
141	33 139 140	syl2anr	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ∧ X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) ) → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card )
142	141	expr	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) → ( X 𝑥 ∈ 𝑦 𝐵 ∈ dom card → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) )
143	31 142	syl9r	⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) → ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) ) )
144	143	expimpd	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ∧ ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) ) )
145	144	ancomsd	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) ) )
146	145	com23	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) ) )
147	146	adantl	⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card → X 𝑥 ∈ 𝑦 𝐵 ∈ dom card ) → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ dom card ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ dom card ) → X 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ dom card ) ) )
148	6 10 23 27 30 147	findcard2s	⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ dom card → X 𝑥 ∈ 𝐴 𝐵 ∈ dom card ) )
149	148	imp	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ dom card ) → X 𝑥 ∈ 𝐴 𝐵 ∈ dom card )

Metamath Proof Explorer

Theorem finixpnum

Proof