fseqdom

Description: One half of fseqen . (Contributed by Mario Carneiro, 18-Nov-2014)

		Ref	Expression
	Assertion	fseqdom	⊢ ( 𝐴 ∈ 𝑉 → ( ω × 𝐴 ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		ovex	⊢ ( 𝐴 ↑_m 𝑛 ) ∈ V
3	1 2	iunex	⊢ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) ∈ V
4		xp1st	⊢ ( 𝑥 ∈ ( ω × 𝐴 ) → ( 1^st ‘ 𝑥 ) ∈ ω )
5		peano2	⊢ ( ( 1^st ‘ 𝑥 ) ∈ ω → suc ( 1^st ‘ 𝑥 ) ∈ ω )
6	4 5	syl	⊢ ( 𝑥 ∈ ( ω × 𝐴 ) → suc ( 1^st ‘ 𝑥 ) ∈ ω )
7		xp2nd	⊢ ( 𝑥 ∈ ( ω × 𝐴 ) → ( 2^nd ‘ 𝑥 ) ∈ 𝐴 )
8		fconst6g	⊢ ( ( 2^nd ‘ 𝑥 ) ∈ 𝐴 → ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) : suc ( 1^st ‘ 𝑥 ) ⟶ 𝐴 )
9	7 8	syl	⊢ ( 𝑥 ∈ ( ω × 𝐴 ) → ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) : suc ( 1^st ‘ 𝑥 ) ⟶ 𝐴 )
10	9	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( ω × 𝐴 ) ) → ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) : suc ( 1^st ‘ 𝑥 ) ⟶ 𝐴 )
11		elmapg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ suc ( 1^st ‘ 𝑥 ) ∈ ω ) → ( ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) ∈ ( 𝐴 ↑_m suc ( 1^st ‘ 𝑥 ) ) ↔ ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) : suc ( 1^st ‘ 𝑥 ) ⟶ 𝐴 ) )
12	6 11	sylan2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( ω × 𝐴 ) ) → ( ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) ∈ ( 𝐴 ↑_m suc ( 1^st ‘ 𝑥 ) ) ↔ ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) : suc ( 1^st ‘ 𝑥 ) ⟶ 𝐴 ) )
13	10 12	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( ω × 𝐴 ) ) → ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) ∈ ( 𝐴 ↑_m suc ( 1^st ‘ 𝑥 ) ) )
14		oveq2	⊢ ( 𝑛 = suc ( 1^st ‘ 𝑥 ) → ( 𝐴 ↑_m 𝑛 ) = ( 𝐴 ↑_m suc ( 1^st ‘ 𝑥 ) ) )
15	14	eliuni	⊢ ( ( suc ( 1^st ‘ 𝑥 ) ∈ ω ∧ ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) ∈ ( 𝐴 ↑_m suc ( 1^st ‘ 𝑥 ) ) ) → ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
16	6 13 15	syl2an2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( ω × 𝐴 ) ) → ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
17	16	ex	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( ω × 𝐴 ) → ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) ) )
18		nsuceq0	⊢ suc ( 1^st ‘ 𝑥 ) ≠ ∅
19		fvex	⊢ ( 2^nd ‘ 𝑥 ) ∈ V
20	19	snnz	⊢ { ( 2^nd ‘ 𝑥 ) } ≠ ∅
21		xp11	⊢ ( ( suc ( 1^st ‘ 𝑥 ) ≠ ∅ ∧ { ( 2^nd ‘ 𝑥 ) } ≠ ∅ ) → ( ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) = ( suc ( 1^st ‘ 𝑦 ) × { ( 2^nd ‘ 𝑦 ) } ) ↔ ( suc ( 1^st ‘ 𝑥 ) = suc ( 1^st ‘ 𝑦 ) ∧ { ( 2^nd ‘ 𝑥 ) } = { ( 2^nd ‘ 𝑦 ) } ) ) )
22	18 20 21	mp2an	⊢ ( ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) = ( suc ( 1^st ‘ 𝑦 ) × { ( 2^nd ‘ 𝑦 ) } ) ↔ ( suc ( 1^st ‘ 𝑥 ) = suc ( 1^st ‘ 𝑦 ) ∧ { ( 2^nd ‘ 𝑥 ) } = { ( 2^nd ‘ 𝑦 ) } ) )
23		xp1st	⊢ ( 𝑦 ∈ ( ω × 𝐴 ) → ( 1^st ‘ 𝑦 ) ∈ ω )
24		peano4	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ ω ∧ ( 1^st ‘ 𝑦 ) ∈ ω ) → ( suc ( 1^st ‘ 𝑥 ) = suc ( 1^st ‘ 𝑦 ) ↔ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) )
25	4 23 24	syl2an	⊢ ( ( 𝑥 ∈ ( ω × 𝐴 ) ∧ 𝑦 ∈ ( ω × 𝐴 ) ) → ( suc ( 1^st ‘ 𝑥 ) = suc ( 1^st ‘ 𝑦 ) ↔ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) )
26		sneqbg	⊢ ( ( 2^nd ‘ 𝑥 ) ∈ V → ( { ( 2^nd ‘ 𝑥 ) } = { ( 2^nd ‘ 𝑦 ) } ↔ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) )
27	19 26	mp1i	⊢ ( ( 𝑥 ∈ ( ω × 𝐴 ) ∧ 𝑦 ∈ ( ω × 𝐴 ) ) → ( { ( 2^nd ‘ 𝑥 ) } = { ( 2^nd ‘ 𝑦 ) } ↔ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) )
28	25 27	anbi12d	⊢ ( ( 𝑥 ∈ ( ω × 𝐴 ) ∧ 𝑦 ∈ ( ω × 𝐴 ) ) → ( ( suc ( 1^st ‘ 𝑥 ) = suc ( 1^st ‘ 𝑦 ) ∧ { ( 2^nd ‘ 𝑥 ) } = { ( 2^nd ‘ 𝑦 ) } ) ↔ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) )
29	22 28	bitrid	⊢ ( ( 𝑥 ∈ ( ω × 𝐴 ) ∧ 𝑦 ∈ ( ω × 𝐴 ) ) → ( ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) = ( suc ( 1^st ‘ 𝑦 ) × { ( 2^nd ‘ 𝑦 ) } ) ↔ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) )
30		xpopth	⊢ ( ( 𝑥 ∈ ( ω × 𝐴 ) ∧ 𝑦 ∈ ( ω × 𝐴 ) ) → ( ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
31	29 30	bitrd	⊢ ( ( 𝑥 ∈ ( ω × 𝐴 ) ∧ 𝑦 ∈ ( ω × 𝐴 ) ) → ( ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) = ( suc ( 1^st ‘ 𝑦 ) × { ( 2^nd ‘ 𝑦 ) } ) ↔ 𝑥 = 𝑦 ) )
32	31	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ ( ω × 𝐴 ) ∧ 𝑦 ∈ ( ω × 𝐴 ) ) → ( ( suc ( 1^st ‘ 𝑥 ) × { ( 2^nd ‘ 𝑥 ) } ) = ( suc ( 1^st ‘ 𝑦 ) × { ( 2^nd ‘ 𝑦 ) } ) ↔ 𝑥 = 𝑦 ) ) )
33	17 32	dom2d	⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) ∈ V → ( ω × 𝐴 ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) ) )
34	3 33	mpi	⊢ ( 𝐴 ∈ 𝑉 → ( ω × 𝐴 ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )

Metamath Proof Explorer

Theorem fseqdom

Proof