fin1a2lem12 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fin1a2lem12		Structured version Visualization version GIF version

Theorem fin1a2lem12 10493

Description: Lemma for fin1a2 10497. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)

**Assertion**
Ref	Expression
fin1a2lem12	⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Proof of Theorem fin1a2lem12 Dummy variables 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 490	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐵 ∈ Fin^III)
2		simpll1 1231	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ⊆ 𝒫 𝐵)
3	2	adantr 486	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → 𝐴 ⊆ 𝒫 𝐵)
4		ssrab2 4005	. . . . . . . 8 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐴
5	4	unissi 4875	. . . . . . 7 ⊢ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ ∪ 𝐴
6		sspwuni 5059	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)
7	6	biimpi 219	. . . . . . 7 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ 𝐴 ⊆ 𝐵)
8	5, 7	sstrid 3919	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
9	3, 8	syl 18	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
10		elpw2g 5294	. . . . . 6 ⊢ (𝐵 ∈ Fin^III → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
11	10	ad2antlr 740	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
12	9, 11	mpbird 260	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵)
13	12	fmpttd 7116	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵)
14		vex 3454	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
15	14	sucex 7821	. . . . . . . . . 10 ⊢ suc 𝑑 ∈ V
16		sssucid 6445	. . . . . . . . . 10 ⊢ 𝑑 ⊆ suc 𝑑
17		ssdomg 9031	. . . . . . . . . 10 ⊢ (suc 𝑑 ∈ V → (𝑑 ⊆ suc 𝑑 → 𝑑 ≼ suc 𝑑))
18	15, 16, 17	mp2 9	. . . . . . . . 9 ⊢ 𝑑 ≼ suc 𝑑
19		domtr 9038	. . . . . . . . 9 ⊢ ((𝑓 ≼ 𝑑 ∧ 𝑑 ≼ suc 𝑑) → 𝑓 ≼ suc 𝑑)
20	18, 19	mpan2 704	. . . . . . . 8 ⊢ (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑)
21	20	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐴 → (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑))
22	21	ss2rabi 4001	. . . . . 6 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑}
23		uniss 4874	. . . . . 6 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
24	22, 23	mp1i 14	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
25		id 23	. . . . . 6 ⊢ (𝑑 ∈ ω → 𝑑 ∈ ω)
26		pwexg 5339	. . . . . . . . 9 ⊢ (𝐵 ∈ Fin^III → 𝒫 𝐵 ∈ V)
27	26	adantl 487	. . . . . . . 8 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝒫 𝐵 ∈ V)
28	27, 2	ssexd 5285	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ∈ V)
29		rabexg 5298	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
30		uniexg 7758	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
31	28, 29, 30	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
32		breq2 5106	. . . . . . . . 9 ⊢ (𝑒 = 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ 𝑑))
33	32	rabbidv 3419	. . . . . . . 8 ⊢ (𝑒 = 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
34	33	unieqd 4879	. . . . . . 7 ⊢ (𝑒 = 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
35		eqid 2760	. . . . . . 7 ⊢ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})
36	34, 35	fvmptg 6992	. . . . . 6 ⊢ ((𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
37	25, 31, 36	syl2anr 609	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
38		peano2 7902	. . . . . 6 ⊢ (𝑑 ∈ ω → suc 𝑑 ∈ ω)
39		rabexg 5298	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
40		uniexg 7758	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
41	28, 39, 40	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
42		breq2 5106	. . . . . . . . 9 ⊢ (𝑒 = suc 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ suc 𝑑))
43	42	rabbidv 3419	. . . . . . . 8 ⊢ (𝑒 = suc 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
44	43	unieqd 4879	. . . . . . 7 ⊢ (𝑒 = suc 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
45	44, 35	fvmptg 6992	. . . . . 6 ⊢ ((suc 𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
46	38, 41, 45	syl2anr 609	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
47	24, 37, 46	3sstr4d 3963	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
48	47	ralrimiva 3154	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
49		fin34i 10463	. . 3 ⊢ ((𝐵 ∈ Fin^III ∧ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵 ∧ ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑)) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
50	1, 13, 48, 49	syl3anc 1398	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
51		fin1a2lem11 10492	. . . . . 6 ⊢ (( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
52	51	adantrr 730	. . . . 5 ⊢ (( [⊊] Or 𝐴 ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
53	52	3ad2antl2 1205	. . . 4 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
54	53	adantr 486	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
55		simpll3 1233	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 ∈ 𝐴)
56		simplrr 790	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ≠ ∅)
57		sspwuni 5059	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 ⊆ ∅)
58		ss0b 4350	. . . . . . . . . . 11 ⊢ (∪ 𝐴 ⊆ ∅ ↔ ∪ 𝐴 = ∅)
59	57, 58	bitri 278	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 = ∅)
60		pw0 4829	. . . . . . . . . . . . 13 ⊢ 𝒫 ∅ = {∅}
61	60	sseq2i 3937	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ {∅})
62		sssn 4781	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
63	61, 62	bitri 278	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
64		df-ne 2956	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
65		0ex 5260	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
66	65	unisn 4885	. . . . . . . . . . . . . . . 16 ⊢ ∪ {∅} = ∅
67	65	snid 4619	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ {∅}
68	66, 67	eqeltri 2856	. . . . . . . . . . . . . . 15 ⊢ ∪ {∅} ∈ {∅}
69		unieq 4877	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → ∪ 𝐴 = ∪ {∅})
70		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → 𝐴 = {∅})
71	69, 70	eleq12d 2854	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = {∅} → (∪ 𝐴 ∈ 𝐴 ↔ ∪ {∅} ∈ {∅}))
72	68, 71	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝐴 = {∅} → ∪ 𝐴 ∈ 𝐴)
73	72	orim2i 924	. . . . . . . . . . . . 13 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 = ∅ ∨ ∪ 𝐴 ∈ 𝐴))
74	73	ord 878	. . . . . . . . . . . 12 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (¬ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
75	64, 74	biimtrid 245	. . . . . . . . . . 11 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
76	63, 75	sylbi 220	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
77	59, 76	sylbir 238	. . . . . . . . 9 ⊢ (∪ 𝐴 = ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
78	77	com12 33	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (∪ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
79	78	con3d 153	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (¬ ∪ 𝐴 ∈ 𝐴 → ¬ ∪ 𝐴 = ∅))
80	56, 55, 79	sylc 66	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 = ∅)
81		ioran 999	. . . . . 6 ⊢ (¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅) ↔ (¬ ∪ 𝐴 ∈ 𝐴 ∧ ¬ ∪ 𝐴 = ∅))
82	55, 80, 81	sylanbrc 595	. . . . 5 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
83		uniun 4889	. . . . . . . 8 ⊢ ∪ (𝐴 ∪ {∅}) = (∪ 𝐴 ∪ ∪ {∅})
84	66	uneq2i 4164	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∪ {∅}) = (∪ 𝐴 ∪ ∅)
85		un0 4343	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∅) = ∪ 𝐴
86	83, 84, 85	3eqtri 2787	. . . . . . 7 ⊢ ∪ (𝐴 ∪ {∅}) = ∪ 𝐴
87	86	eleq1i 2851	. . . . . 6 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ ∪ 𝐴 ∈ (𝐴 ∪ {∅}))
88		elun 4152	. . . . . 6 ⊢ (∪ 𝐴 ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}))
89	65	elsn2 4622	. . . . . . 7 ⊢ (∪ 𝐴 ∈ {∅} ↔ ∪ 𝐴 = ∅)
90	89	orbi2i 926	. . . . . 6 ⊢ ((∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
91	87, 88, 90	3bitri 300	. . . . 5 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
92	82, 91	sylnibr 332	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}))
93		unieq 4877	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = ∪ (𝐴 ∪ {∅}))
94		id 23	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
95	93, 94	eleq12d 2854	. . . . 5 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
96	95	notbid 321	. . . 4 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
97	92, 96	syl5ibrcom 250	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})))
98	54, 97	mpd 16	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
99	50, 98	pm2.65da 829	1 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 {crab 3412 Vcvv 3450 ⊆ wss 3895 ∪ cun 4149 ∅c0 4278 𝒫 cpw 4556 {csn 4584 ∪ cuni 4866 class class class wbr 5102 ↦ cmpt 5185 Or wor 5557 ran crn 5651 suc csuc 6364 ⟶wf 6535 ‘cfv 6539 [⊊] crpss 7739 ωcom 7878 ≼ cdom 8975 Fincfn 8977 Fin^IIIcfin3 10363

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-rpss 7740 df-om 7879 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-er 8721 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-wdom 9563 df-card 10024 df-fin4 10369 df-fin3 10370

This theorem is used by: fin1a2s 10496

W3C validator