numiunnum

Description: An indexed union of sets is numerable if its index set is numerable and there exists a collection of well-orderings on its members. (Contributed by Matthew House, 23-Aug-2025)

		Ref	Expression
	Assertion	numiunnum	⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		dfac8b	⊢ ( 𝐴 ∈ dom card → ∃ 𝑠 𝑠 We 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) → ∃ 𝑠 𝑠 We 𝐴 )
3		simpll	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → 𝐴 ∈ dom card )
4		simplr	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) )
5		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 ) )
6	4 5	sylib	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 ) )
7	6	simpld	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
8		iunexg	⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
9	3 7 8	syl2anc	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
10	9 9	xpexd	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ V )
11		opabssxp	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 × ∪ 𝑥 ∈ 𝐴 𝐵 )
12	11	a1i	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 × ∪ 𝑥 ∈ 𝐴 𝐵 ) )
13	10 12	ssexd	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } ∈ V )
14		simpr	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → 𝑠 We 𝐴 )
15		exse	⊢ ( 𝐴 ∈ dom card → 𝑠 Se 𝐴 )
16	15	ad2antrr	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → 𝑠 Se 𝐴 )
17	6	simprd	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 )
18		eqid	⊢ ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) )
19		eqid	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
20	18 19	weiunwe	⊢ ( ( 𝑠 We 𝐴 ∧ 𝑠 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } We ∪ 𝑥 ∈ 𝐴 𝐵 )
21	14 16 17 20	syl3anc	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } We ∪ 𝑥 ∈ 𝐴 𝐵 )
22		weeq1	⊢ ( 𝑡 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } → ( 𝑡 We ∪ 𝑥 ∈ 𝐴 𝐵 ↔ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) 𝑠 ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∨ ( ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑧 ) ∧ 𝑦 ⦋ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑠 𝑢 ) ) ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } We ∪ 𝑥 ∈ 𝐴 𝐵 ) )
23	13 21 22	spcedv	⊢ ( ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) ∧ 𝑠 We 𝐴 ) → ∃ 𝑡 𝑡 We ∪ 𝑥 ∈ 𝐴 𝐵 )
24	2 23	exlimddv	⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) → ∃ 𝑡 𝑡 We ∪ 𝑥 ∈ 𝐴 𝐵 )
25		ween	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ dom card ↔ ∃ 𝑡 𝑡 We ∪ 𝑥 ∈ 𝐴 𝐵 )
26	24 25	sylibr	⊢ ( ( 𝐴 ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ dom card )

Metamath Proof Explorer

Theorem numiunnum

Proof