Metamath Proof Explorer

Theorem ldsysgenld

Description: The intersection of all lambda-systems containing a given collection of sets A , which is called the lambda-system generated by A , is itself also a lambda-system. (Contributed by Thierry Arnoux, 16-Jun-2020)

Ref Expression
Hypotheses isldsys.l ⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
ldsysgenld.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
ldsysgenld.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝒫 𝑂 )
Assertion ldsysgenld ( 𝜑 → ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∈ 𝐿 )

Proof

Step Hyp Ref Expression
1 isldsys.l ⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
2 ldsysgenld.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
3 ldsysgenld.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝒫 𝑂 )
4 pwsiga ⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ ( sigAlgebra ‘ 𝑂 ) )
5 2 4 syl ⊢ ( 𝜑 → 𝒫 𝑂 ∈ ( sigAlgebra ‘ 𝑂 ) )
6 1 sigaldsys ⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝐿
7 6 5 sselid ⊢ ( 𝜑 → 𝒫 𝑂 ∈ 𝐿 )
8 sseq2 ⊢ ( 𝑡 = 𝒫 𝑂 → ( 𝐴 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝒫 𝑂 ) )
9 8 elrab ⊢ ( 𝒫 𝑂 ∈ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ↔ ( 𝒫 𝑂 ∈ 𝐿 ∧ 𝐴 ⊆ 𝒫 𝑂 ) )
10 7 3 9 sylanbrc ⊢ ( 𝜑 → 𝒫 𝑂 ∈ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
11 intss1 ⊢ ( 𝒫 𝑂 ∈ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } → ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ⊆ 𝒫 𝑂 )
12 10 11 syl ⊢ ( 𝜑 → ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ⊆ 𝒫 𝑂 )
13 5 12 sselpwd ⊢ ( 𝜑 → ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∈ 𝒫 𝒫 𝑂 )
14 1 isldsys ⊢ ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ) )
15 14 simprbi ⊢ ( 𝑡 ∈ 𝐿 → ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) )
16 15 simp1d ⊢ ( 𝑡 ∈ 𝐿 → ∅ ∈ 𝑡 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ∅ ∈ 𝑡 )
18 17 a1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( 𝐴 ⊆ 𝑡 → ∅ ∈ 𝑡 ) )
19 18 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → ∅ ∈ 𝑡 ) )
20 0ex ⊢ ∅ ∈ V
21 20 elintrab ⊢ ( ∅ ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → ∅ ∈ 𝑡 ) )
22 19 21 sylibr ⊢ ( 𝜑 → ∅ ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
23 nfv ⊢ Ⅎ 𝑡 𝜑
24 nfcv ⊢ Ⅎ 𝑡 𝑥
25 nfrab1 ⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 }
26 25 nfint ⊢ Ⅎ 𝑡 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 }
27 24 26 nfel ⊢ Ⅎ 𝑡 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 }
28 23 27 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
29 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → 𝑡 ∈ 𝐿 )
30 vex ⊢ 𝑥 ∈ V
31 30 elintrab ⊢ ( 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → 𝑥 ∈ 𝑡 ) )
32 31 biimpi ⊢ ( 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } → ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → 𝑥 ∈ 𝑡 ) )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → 𝑥 ∈ 𝑡 ) )
34 33 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ 𝑡 ∈ 𝐿 ) → ( 𝐴 ⊆ 𝑡 → 𝑥 ∈ 𝑡 ) )
35 34 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → 𝑥 ∈ 𝑡 )
36 15 simp2d ⊢ ( 𝑡 ∈ 𝐿 → ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
37 36 r19.21bi ⊢ ( ( 𝑡 ∈ 𝐿 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
38 29 35 37 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
39 38 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ 𝑡 ∈ 𝐿 ) → ( 𝐴 ⊆ 𝑡 → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ) )
40 39 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → ( 𝑡 ∈ 𝐿 → ( 𝐴 ⊆ 𝑡 → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ) ) )
41 28 40 ralrimi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ) )
42 difexg ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑂 ∖ 𝑥 ) ∈ V )
43 elintrabg ⊢ ( ( 𝑂 ∖ 𝑥 ) ∈ V → ( ( 𝑂 ∖ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ) ) )
44 2 42 43 3syl ⊢ ( 𝜑 → ( ( 𝑂 ∖ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ) ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → ( ( 𝑂 ∖ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ) ) )
46 41 45 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → ( 𝑂 ∖ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
47 46 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ( 𝑂 ∖ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
48 26 nfpw ⊢ Ⅎ 𝑡 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 }
49 24 48 nfel ⊢ Ⅎ 𝑡 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 }
50 23 49 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
51 nfv ⊢ Ⅎ 𝑡 ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 )
52 50 51 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
53 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → 𝑡 ∈ 𝐿 )
54 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) ∧ 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
55 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) ∧ 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → 𝑡 ∈ 𝐿 )
56 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) ∧ 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → 𝐴 ⊆ 𝑡 )
57 vex ⊢ 𝑢 ∈ V
58 57 elintrab ⊢ ( 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → 𝑢 ∈ 𝑡 ) )
59 58 biimpi ⊢ ( 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } → ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → 𝑢 ∈ 𝑡 ) )
60 59 r19.21bi ⊢ ( ( 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∧ 𝑡 ∈ 𝐿 ) → ( 𝐴 ⊆ 𝑡 → 𝑢 ∈ 𝑡 ) )
61 60 imp ⊢ ( ( ( 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → 𝑢 ∈ 𝑡 )
62 54 55 56 61 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) ∧ 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → 𝑢 ∈ 𝑡 )
63 62 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → ( 𝑢 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } → 𝑢 ∈ 𝑡 ) )
64 63 ssrdv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ⊆ 𝑡 )
65 64 sspwd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ⊆ 𝒫 𝑡 )
66 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
67 65 66 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → 𝑥 ∈ 𝒫 𝑡 )
68 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
69 15 simp3d ⊢ ( 𝑡 ∈ 𝐿 → ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
70 69 r19.21bi ⊢ ( ( 𝑡 ∈ 𝐿 ∧ 𝑥 ∈ 𝒫 𝑡 ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
71 70 imp ⊢ ( ( ( 𝑡 ∈ 𝐿 ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ∪ 𝑥 ∈ 𝑡 )
72 53 67 68 71 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝐴 ⊆ 𝑡 ) → ∪ 𝑥 ∈ 𝑡 )
73 72 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) → ( 𝐴 ⊆ 𝑡 → ∪ 𝑥 ∈ 𝑡 ) )
74 73 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑡 ∈ 𝐿 → ( 𝐴 ⊆ 𝑡 → ∪ 𝑥 ∈ 𝑡 ) ) )
75 52 74 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → ∪ 𝑥 ∈ 𝑡 ) )
76 vuniex ⊢ ∪ 𝑥 ∈ V
77 76 elintrab ⊢ ( ∪ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝐴 ⊆ 𝑡 → ∪ 𝑥 ∈ 𝑡 ) )
78 75 77 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ∪ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } )
79 78 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) )
80 79 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) )
81 22 47 80 3jca ⊢ ( 𝜑 → ( ∅ ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∧ ∀ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ( 𝑂 ∖ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∧ ∀ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ) )
82 13 81 jca ⊢ ( 𝜑 → ( ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∧ ∀ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ( 𝑂 ∖ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∧ ∀ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ) ) )
83 1 isldsys ⊢ ( ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∈ 𝐿 ↔ ( ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∧ ∀ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ( 𝑂 ∖ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∧ ∀ 𝑥 ∈ 𝒫 ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ) ) ) )
84 82 83 sylibr ⊢ ( 𝜑 → ∩ { 𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡 } ∈ 𝐿 )